[Agda] I'm not sure... case for the constructor ..., because
I get stuck when trying to solve...
Andreas Abel
abela at chalmers.se
Sat Dec 6 09:57:39 CET 2014
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/
More information about the Agda
mailing list