Constraint solving could be more flexible

[agda]

Constraint solving could be more flexible

[GoogleCodeExporter]

[deleted comment]

[GoogleCodeExporter]

[deleted comment]

[GoogleCodeExporter]

There is probably a problem with constraint solving, but the example above 
isn't it.
There was a problem with the unifying substitution not being applied properly
(fixed), but there's also a problem with the example. A simpler version:

  data D : (k : K)(t : T k) -> Set where
    c : (k : K) -> D k (f k)

  foo : D a ta -> Set
  foo (c a) = K

This is actually not correct. When matching on D a ta the argument to c is 
determined
by typechecking (before you get a chance to match on it) so it should be dotted:

  foo (c .a) = K

Original comment by [email protected] on 24 Oct 2007 at 12:15

• Changed state: New

[GoogleCodeExporter]

Here's an example of the problem:

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

_+_ : Nat -> Nat -> Nat
zero  + m = m
suc n + m = suc (n + m)

data T : Nat -> Nat -> Set where
  c : (x : Nat) -> T x zero

foo : (n m : Nat) -> T (n + m) n -> Set
foo ._ ._ (c m) = Nat

If you flip the arguments to T it goes through.

Original comment by [email protected] on 24 Oct 2007 at 12:31

• Changed state: Accepted

[GoogleCodeExporter]

Original comment by [email protected] on 24 Oct 2007 at 2:15

• Changed state: Fixed