Bound variable not as bound as one would think

[ionescu]

The following type checks

module bind

X : Set

R : X -> X -> Bool

f : (x0 : X) -> (x : X ** so (x0 R x))

test : (x : X) -> Bool
test k = True where
oops : (x' : X ** so (k R x'))
oops = f k

However, replacing |k| with |x| in the definition of |test|, so that we have

test : (x : X) -> Bool
test x = True where
oops : (x' : X ** so (x R x'))
oops = f x

raises a type error:

bind.lidr:12:Can't unify (x' ** so (R x x')) with (x ** so (R x x))

Which then goes away if we replace the name of the bound variable in the type of |f| by, say, |k|:

f : (x0 : X) -> (k : X ** so (x0 R k))

[edwinb]

This turns out to have been a mysterious scoping bug which only arose when type checking things with lambdas in their type that happened to have the same name as something whose scope had previously been resolved. Now fixed.

[nicolabotta]

I am afraid this could be an instance of the same problem, though in a slightly more involved situation. The following code type checks

> module TestBound

> soFalseElim : so False -> a
> soFalseElim x = FalseElim (believe_me x)

> X : Set
> X = (n : Nat ** so (n < 3))

> (==) : X -> X -> Bool
> (==) x x' = (getWitness x == getWitness x')

> data Move = L | R 

> adm : X -> Move -> Bool
> adm (n ** _) L = n <= 1
> adm (n ** _) R = n >= 1

> Y : X -> Set
> Y x = (a : Move ** so (adm x a))

> step : (x : X) -> Y x -> X
> step (O ** _) (L ** _) = (2 ** oh)
> step ((S n) ** _) (L ** _) = (n ** believe_me oh) -- trivial
> step (n ** _) (R ** _) = 
>   if n == 2 then (O ** oh) else (S n ** believe_me oh)

> pred : X -> X -> Bool
> pred x x' = (adm x L && x' == step x (L ** believe_me oh)) ||
>             (adm x R && x' == step x (R ** believe_me oh))

> succs : X -> (n : Nat ** Vect X n)
> succs x = filter (pred x) [(0 ** oh),(1 ** oh),(2 ** oh)]

> preds : X -> (n : Nat ** Vect X n)
> preds x' = filter ((flip pred) x') [(0 ** oh),(1 ** oh),(2 ** oh)]

> emptyC : (n : Nat ** Vect X n) -> Bool
> emptyC (_ ** Nil) = True
> emptyC (_ ** (x :: xs)) = False

> inC : X -> (n : Nat ** Vect X n) -> Bool
> inC _ (_ ** Nil) = False
> inC x (_ ** (x' :: xs')) = x == x' || inC x (_ ** xs')

> someC : (X -> Bool) -> (n : Nat ** Vect X n) -> Bool
> someC _ (_ ** Nil) = False
> someC p (_ ** (x :: xs)) = p x || someC p (_ ** xs)

> lemmaC2 : (xs : (n : Nat ** Vect X n)) ->
>           so (not (emptyC xs)) ->
>           (x : X ** so (x `inC` xs))
> lemmaC2 (_ ** Nil) soF = soFalseElim soF
> lemmaC2 (_ ** (x :: xs)) _ = (x ** believe_me oh)

> lemmaC3 : (x : X) ->
>           (p : X -> Bool) ->
>           (xs : (n : Nat ** Vect X n)) ->
>           so (p x) ->
>           so (inC x xs) ->
>           so (someC p xs)
> lemmaC3 _ _ (_ ** Nil) _ soF = soFalseElim soF
> lemmaC3 _ _ (_ ** (x :: xs)) _ _ = ?lemmaC3_2

> succsTh : (x : X) -> so (not (emptyC (succs x)))
> succsTh x = ?lala

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

> viable : (n : Nat) -> X -> Bool
> viable O _ = True
> viable (S n) x = someC (viable n) (succs x)

> viableTh : (n : Nat) -> (x : X) -> so (viable n x)
> viableTh O _ = oh
> viableTh (S n) k = step2 where  
>   step0 : so (not (emptyC (succs k)))
>   step0 = succsTh k
>   step1 : (x' : X ** so (x' `inC` (succs k)))
>   step1 = lemmaC2 (succs k) step0
>   step2 : so (someC (viable n) (succs k))
>   step2 = lemmaC3 x' (viable n) (succs k) vnx' x'inCsuccsx where
>     x' : X
>     x' = getWitness step1
>     vnx' : so (viable n x')
>     vnx' = viableTh n x' -- induction step
>     x'inCsuccsx : so (x' `inC` (succs k))
>     x'inCsuccsx = getProof step1

But replacing |k| with |x| in the second pattern of the definition of |viableTh| yields

test_bound.lidr:81:Can't unify (x' ** so (inC x' ...)) with (x ** so (inC x ...))

Maybe re-open the issue ?

[nicolabotta]

There was a rendering error in the above message (I used |pre| instead of |````| to mark code) which made the code unusable. It should type check, now.