"WellFounded" relation passes totality check, builds and hangs

[michaeljklein]

I found a way to implement arbitrary coercion between types by using an infinite loop that type checks as a WellFounded relation.

Steps to Reproduce

» idris -v
1.3.1

||| WellFoundedLoop.idr
%default total

data FreeAccessible : {a:Type} -> (x:a) -> (y:a) -> Type where
  FreeAccess : {a:Type} -> {x:a} -> {y:a}
            -> Accessible FreeAccessible x
            -> FreeAccessible x y

implementation WellFounded (FreeAccessible {a}) where
  wellFounded x = Access (\y, (FreeAccess {x} {y} access') => access')

freeAccess : {a:Type} -> (x:a) -> (y:a) -> FreeAccessible {a} x y
freeAccess x y = FreeAccess {x} {y} (wellFounded x)

freeRec : {a:Type} -> (step : (x : a) -> ((y : a) -> b) -> b) -> a -> b
freeRec step =
  wfRec {rel=FreeAccessible} (\x, f => step x (\y => f y (freeAccess y x)))

coerce : {a:Type} -> {b:Type} -> a -> b
coerce = freeRec (\x, f => f x)

main : IO ()
main = coerce ()

To build:

idris --total --V2 WellFoundedLoop.idr -o WellFoundedLoop

Expected Behavior

The module should neither type check nor compile.

Observed Behavior

» idris --total --V2 WellFoundedLoop.idr -o WellFoundedLoop
Reading ./WellFoundedLoop.idr
Type checking ./WellFoundedLoop.idr
Totality checking ./WellFoundedLoop.idr
Universe checking ./WellFoundedLoop.idr
Writing IBC for: "./WellFoundedLoop.ibc"
Compiling Output.
Running Erasure Analysis
Defunctionalising
Inlining
Generating Code.
» time ./WellFoundedLoop
^C
./WellFoundedLoop  121.48s user 0.50s system 99% cpu 2:02.55 total