[Agda] I'm not sure... case for the constructor ..., because I get stuck when trying to solve...

[Dmytro Starosud]

Thanks, Andreas,

I had a kind of similar thoughts, but needed confirmation.
So, the rule is "do not use functional dependencies as a family indexes,
but just constructors".
Please correct if this is not accurate statement.

What is the root cause (I mean what difficulties in compiler/theory) which
sometimes doesn't allow solving such unification problems?

Thanks a lot,
Dmytro


2014-12-06 10:57 GMT+02:00 Andreas Abel <abela at chalmers.se>:

> The problem is that you are indexing your family Term by non-patterns in
> some of the constructor cases.  Then Agda can sometimes not solve the
> unification constraints involved in dependent pattern matching, and gives
> up or produces error messages.  The solution is to use explicit proofs of
> equality in your constructors instead.
>
> Here is a cut-down version of your plight:
>
> module _ where
>
> open import Data.Bool
> open import Relation.Binary.PropositionalEquality
>
> module NonPatternFamily where
>
>   data Term : Bool → Set where
>     I : Term false
>     App : (a b : Bool) → Term a → Term b → Term (a ∨ b)
>       -- Non-pattern in target of App
>       -- _∨_ is a defined function, not a constructor.
>
>   fails : Term false → Set
>   fails (App false false I x) = Bool
>   fails _ = Bool
>
>   -- a ∨ b != false of type Bool
>   -- when checking that the pattern App false false I x has type
>   -- Term false
>
> -- Radical fix: no index to Term, just parameter:
>
> module JustData where
>
>   -- Version with no indices at all, only parameters.
>
>   data Term (i : Bool) : Set where
>     I   : i ≡ false → Term i
>     App : (a b : Bool) → i ≡ a ∨ b → Term a → Term b → Term i
>
>   test : Term false → Set
>   test (App false false refl (I refl) x) = Bool
>   test _ = Bool
>
> -- Moderate fix: retain the index in harmless (pattern case).
>
> module PatternFamily where
>
>   -- Version with index,
>   -- but using equality when non-pattern index would be needed.
>
>   data Term : (i : Bool) → Set where
>     I   : Term false
>     App : (i a b : Bool) → i ≡ a ∨ b → Term a → Term b → Term i
>
>   test : Term false → Set
>   test (App .false false false refl I x) = Bool
>   test _ = Bool
>
> Hope that helps,
> Andreas
>
>
>
> On 05.12.2014 22:47, Dmytro Starosud wrote:
>
>> Hello guys,
>>
>> I am trying to write a function on indexed types:
>> https://gist.github.com/dima-starosud/7100947b0e243ea6a034
>> But I cannot understand the reason of the error messages shown, and how
>> to solve issues arisen.
>>
>> Please see a gist (link above).
>> Ideally I wanted "reduce₁". But that didn't compile. (And I think I can
>> imagine the reason why)
>>
>> Next attempt was "reduce₂". But this would involve a lot of unnecessary
>> code on RHSs.
>>
>> Than I decided to improve it and got "reduce₃", but it gave me
>> completely puzzling error message.
>>
>> Please help me to understand all that stuff Agda communicates to me.
>>
>> I would like something really simple (like "reduce₁"), probably with
>> help of *pattern*s.
>>
>> Thanks in advance,
>> Dmytro
>>
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141206/cd531338/attachment.html