Segfault in LinearCheck and two other issues

[timsueberkrueb]

Hey, I stumbled upon some issues while working through plfa, chapter DeBruijn. Note that the code below compiles fine in Idris 1 but Idris 2 has some problems with it.

import Data.Vect

data Typ : Type where
    TLam : Typ -> Typ -> Typ
    TNat : Typ

data Term : Typ -> Vect len Typ -> Type where
    Var : Elem a ctx -> Term a ctx
    Lam : Term b (a :: ctx) -> Term (TLam a b) ctx
    Fix : Term a (a :: ctx) -> Term a ctx

lookup : Vect len Typ -> Fin len -> Typ
lookup (a :: ctx) FZ = a
lookup (_ :: ctx) (FS n) = lookup ctx n

count : {ctx : Vect len Typ} -> (n : Fin len) -> Elem (lookup ctx n) ctx
count {ctx = _ :: ctx} FZ = Here
count {ctx = _ :: ctx} (FS n) = There (count n)

... this compiles just fine. Here comes the trouble:

Problem 1

segfaults : Term (TLam TNat TNat) ctx
segfaults = Fix (Lam (Var (count 0)))

“idris2 cycleIssue.idr” terminated by signal SIGSEGV (Address boundary error)

Program received signal SIGSEGV, Segmentation fault.
0x000000000045a302 in _idris__123_APPLY_95_0_125_ ()
(gdb) bt
#0  0x000000000045a302 in _idris__123_APPLY_95_0_125_ ()
#1  0x0000000000997363 in _idris_Core_46_LinearCheck_46_lcheck ()
#2  0x0000000000996f68 in _idris_Core_46_LinearCheck_46_lcheck ()
#3  0x0000000000996f68 in _idris_Core_46_LinearCheck_46_lcheck ()
#4  0x0000000000996f68 in _idris_Core_46_LinearCheck_46_lcheck ()
#5  0x00000000009979c7 in _idris_Core_46_LinearCheck_46_lcheck ()
#6  0x0000000000996f68 in _idris_Core_46_LinearCheck_46_lcheck ()
#7  0x00000000009979c7 in _idris_Core_46_LinearCheck_46_lcheck ()
#8  0x00000000009979c7 in _idris_Core_46_LinearCheck_46_lcheck ()
#9  0x0000000000996f68 in _idris_Core_46_LinearCheck_46_lcheck ()
#10 0x00000000009979c7 in _idris_Core_46_LinearCheck_46_lcheck ()
(...)

Problem 2 (probably #68)

cycleDetected : Term (TLam TNat TNat) ctx
cycleDetected = Fix (Var (count 0))

Uncaught error: cycleIssue.idr:24:22--24:35:Cycle detected in metavariable solution $resolved2458

Problem 3 (probably #302)

notAccessible : Term (TLam TNat (TLam TNat TNat)) ctx
notAccessible = Lam (Lam (Var (count 0)))

cycleIssue.idr:21:17--23:1:While processing right hand side of notAccessible at cycleIssue.idr:21:1--23:1:
ctx is not accessible in this context

[ziman]

Problem #3 is an interesting one and it's different from #302.

The right way to go would be changing the type of count to start with count : {0 ctx : Vect len Typ} -> .... That should check because the constructor tag is forced and its fields end up unused or in erased recursive positions. (This is easily visible in the compiled form of count: there's a single-branch case match on the vector, and all its fields are unused, except for its tail in the recursive call.)

However, it does not check currently; probably because the implemented rules are a bit too strict.

[edwinb]

Problem 3 at least is because ctx has unrestricted usage in the type of count, but you've said you're not going to use it in the type of notAccessible. There may be some more complicated reason why it's not needed, as @ziman says, but usage checking beyond what's in the type is quite conservative.

[timsueberkrueb]

Ah, I see. Explicitly specifying len and ctx works:

notAccessible : {len : Nat} -> {ctx : Vect len Typ} -> Term (TLam TNat (TLam TNat TNat)) ctx
notAccessible = Lam (Lam (Var (count 0)))

[edwinb]

Okay, I see what's going on here. Essentially, it means I need to implement the occurs check properly, which is something I've meant to do for ages. What it was trying to do was solve this constraint:

?ctx =?= TLam TNat (lookup (TNat :: ?ctx) FZ) :: ctx

...and the naive solution has a cycle because the definition uses ?ctx itself. This is okay in Idris 1 because it normalises all over the place, and normalising the RHS of this equation evaluates lookup, so it just resolves to TLam TNat TNat :: ctx, which is what we want.

I've implemented a fix, though I haven't run all the tests yet, so expect a patch soonish. Hopefully it's related to #68, I'll test that later.

[timsueberkrueb]

Awesome, thank you. Here is the complete file in case that can help with testing the patch: https://gist.github.com/timsueberkrueb/5275cb940258f833800fd7c864f81759