[Agda] exhaustive patterns

[Serge D. Mechveliani]

On Tue, Feb 19, 2013 at 12:18:33AM +0100, Andreas Abel wrote:
> The reason you cannot replace 'nothing' with an underscore '_' is
> that Agda first checks that each individual clause is well-typed,
> and only then does a coverage check which would reveal that '_' must
> actually be 'nothing'.
> 
> Since '_' is just a variable, the emptyness check fails, which
> succeeds with the more informative 'nothing'.
> 
> Does this help?
> 

Thank you. I understand now how it works.
But may be it is better for the language to put that each clause is 
checked with taking in account previousely checked clauses
?
This will extend the sugar of wildcard, because in such a situtation the 
checker will replace `_' with the single remaining constructor.

I do not know, may be this will lead to various complications in the type 
check (which, I expect, is already very complex).

Regards,

------
Sergei

 
> Am 18.02.2013 18:06, schrieb Serge D. Mechveliani:
> >Dear all,
> >
> >I have a question about the fragment
> >
> >  inverse : (a : C) -> Inverse {M = Mg} e a
> >  inverse a  with  invMb a | inversionIsTotal a _
> >  ...      | just (yes inv) | _  = inv
> >  ...      | just (no _)    | ()
> >  ...      | nothing        | ()
> >
> >It is type-checked in  Agda-2.3.2 MAlonzo,
> >
> >while changing the last line to      ...  | _ | ()
> >leads to the report
> >
> >" Checking AlgClasses1
> >(/home/mechvel/doconA/0.01/source/AlgClasses1.agda).
> >  Finished AlgClasses1.
> >
> >Failed to solve the following constraints:
> >  [0] Is empty: justYes? .w \equiv┴║ Data.Bool.true
> >"
> >
> >(without printing the line number).
> >
> >This looks strange, because the pattern set
> >                            {just (yes inv), just (no _), nothing}
> >
> >is exhaustive for the type of  Maybe $ Dec $ Inverse {M = Mg} e a
> >of  invMb a,
> >hence the last wildcard needs to be replaced with `nothing'.
> >
> >Am I missing something?
> >
> >Regards,
> >
> >------
> >Sergei
> >
> >_______________________________________________
> >Agda mailing list
> >Agda at lists.chalmers.se
> >https://lists.chalmers.se/mailman/listinfo/agda
> 
> -- 
> Andreas Abel  <><     Du bist der geliebte Mensch.
> 
> Theoretical Computer Science, University of Munich
> http://www.tcs.informatik.uni-muenchen.de/~abel/
>