search

idris-lang / Idris-dev

A Dependently Typed Functional Programming Language
http://idris-lang.org
Other
3.43k stars 643 forks source link

"Can't verify injectivity" error #74

Closed nicolabotta closed 11 years ago

nicolabotta commented 11 years ago

The appended code fails to type check with

test_injective.lidr:41:Can't verify injectivity of reachable m when unifying so (reachable m x) and so (p x)

I'm probably missing something but I do not see why |reachable m| is required to be injective (which in general is not) for |lemmaC3| to apply. The code type checks if line 41 is commented out and line 42 is uncommented.

module TestInjective

X : Set Y : X -> Set step : (x : X) -> Y x -> X

C : Set -> Set inC : X -> C X -> Bool someC : (X -> Bool) -> C X -> Bool lemmaC3 : (x : X) -> (p : X -> Bool) -> (xs : C X) -> so (p x) -> so (x inC xs) -> so (someC p xs)

preds : X -> C X lemmaPreds1 : (x : X) -> (y : Y x) -> so (x inC (preds (step x y)))

reachable : (m : Nat) -> X -> Bool reachable O _ = True reachable (S m) x' = someC (reachable m) (preds x')

reachableTh : (m : Nat) -> (x : X) -> so (reachable m x) -> (y : Y x) -> so (reachable (S m) (step x y)) reachableTh m x rmx y = step3 where xs : C X xs = preds (step x y) step1 : so (x inC xs) step1 = lemmaPreds1 x y p : X -> Bool p = reachable m px : so (p x) px = rmx step2 : so (someC p xs) step2 = lemmaC3 x p xs px step1 -- step2 = ?reachableTh_step2 step3 : so (reachable (S m) (step x y)) step3 = step2

edwinb commented 11 years ago

I've worked out what's going on here - simply that elaboration happens in the wrong order, so when applying lemmaC3 it doesn't yet know that the p argument has to be reachable - but I'm not totally happy with my solution to it even though all the tests pass and libraries build...

There was previously a bit of a hack on elaboration order of arguments, to do arguments that informed the rest of elabroation most, earlier, but now it's a bit cleverer about postponing unification problems, I'm not sure it's necessary.

I have pushed a patch - let me know if it breaks anything else (it doesn't for me though).

nicolabotta commented 11 years ago

Edwin Brady notifications@github.com wrote:

I have pushed a patch - let me know if it breaks anything else (it doesn't for me though).

Edwin,

so far everything seems to work very nicely, thanks !

I'm still at home with a bad cold but I'll go back to the real code asap and check the impact of the new improvements.

I still have not opened an issue on the linear vs exponential complexity problem because I thought it was of a somehow different nature. If you like me to do so, please let me know.

Best, Nicola