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: d34cf6261
Steps to Reproduce
Type check the snippet.
Uncomment the definition of oops.
Type check the snippet again.
Uncomment the definition of uhOh.
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.
Uncommenting
oops
oruhOh
and then type checking causes Idris to loop indefinitely.Environment
Idris commit: d34cf6261
Steps to Reproduce
oops
.uhOh
.Expected Behavior
Idris should accept the program as correct after uncommenting
oops
. It should provide a type error when uncommentinguhOh
.Observed Behavior
Idris will enter a seemingly infinite loop when uncommenting either definition.
Further Details
Idris works correctly for
oops
if you inline eitherPred
orfix
.The problem remains for
oops
if you:import Data.Stream
to provideiterate
andindex
Pred
more complex (in my original use case,Pred = Nat -> Type
)No changes I have tried have caused
uhOh
to terminate.