"Can't verify injectivity" error

[nicolabotta]

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]

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]

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