Type checker does not terminate when comparing codata types.

[yellowsquid]

Uncommenting oops or uhOh and then type checking causes Idris to loop indefinitely.

index : Nat -> Stream a -> a
index 0     (x :: xs) = x
index (S k) (x :: xs) = index k xs

iterate : (a -> a) -> a -> Stream a
iterate f x = x :: iterate f (f x)

Pred : Type
Pred = Type

fix : (Pred -> Pred) -> Pred
fix f = (n ** index n (iterate f Void))

oops : {n : Nat} -> index n (iterate f Void) -> fix f
-- oops {n} prf = (n ** prf)

uhOh : {n : Nat} -> index n (iterate f ()) -> index n (iterate f Void)
-- uhOh prf = prf

Environment

Idris commit: d34cf62

Steps to Reproduce

1. Type check the snippet.
2. Uncomment the definition of oops.
3. Type check the snippet again.
4. Uncomment the definition of uhOh.
5. Type check the snippet one last time.

Expected Behavior

Idris should accept the program as correct after uncommenting oops. It should provide a type error when uncommenting uhOh.

Observed Behavior

Idris will enter a seemingly infinite loop when uncommenting either definition.

Further Details

Idris works correctly for oops if you inline either Pred or fix.

The problem remains for oops if you:

• import Data.Stream to provide iterate and index
• make Pred more complex (in my original use case, Pred = Nat -> Type)
• use a custom record instead of dependent pairs

No changes I have tried have caused uhOh to terminate.

[buzden]

Is this #964?

[yellowsquid]

Yes, but the bug when things don't unify seems to be a new observation. Feel free to close this as a duplicate and I'll update the original issue.