"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

[michaeljklein]

I was able to simplify the example:

%default total

||| Isomorphic to: `(a:Type) -> a -> a -> a -> ..`
data Foo : (a:Type) -> Type where
  MkFoo : (a -> Foo a) -> Foo a

||| `f` is derived to be smaller than `MkFoo f`
accFoo : {a:Type} -> {b:Type} -> a -> Foo a -> b
accFoo x (MkFoo f) = accFoo x (f x)

||| `Bar` is isomorphic to `Foo Bar`
data Bar : Type where
  MkBar : Foo Bar -> Bar

runBar : Bar -> Foo Bar
runBar (MkBar fooBar) = fooBar

fooBar : Foo Bar
fooBar = MkFoo runBar

bar : Bar
bar = MkBar fooBar

accBar : {a:Type} -> a
accBar = accFoo bar fooBar

The totality checker detects that certain variants of Foo are not strictly positive as expected:

data CoFoo : (a:Type) -> Type where
  MkCoFoo : (CoFoo a -> a) -> CoFoo a

data EndoFoo : (a:Type) -> Type where
  MkEndoFoo : (EndoFoo a -> EndoFoo a) -> EndoFoo a

But the following variant allows us to define barId, which causes the type-checker to enter an infinite loop and leak memory:

data FooId : (a:Type) -> Type where
  MkFooId : (a -> a) -> FooId a

runFooId : FooId a -> a -> a
runFooId (MkFooId f) = f

||| `BarId` is isomorphic to `BarId -> BarId`
data BarId : Type where
  MkBarId : FooId BarId -> BarId

runBarId : BarId -> FooId BarId
runBarId (MkBarId f) = f

fixBarId : (BarId -> BarId) -> BarId
fixBarId f = f (MkBar (MkFoo f))

barId : BarId
barId = fixBarId (\b => fixBarId (runFooId (runBarId b)))

I'm not sure BarId is the same bug: should I move it to another issue?