Non termination constructing value which contains computation type

[mpickering]

The compiler doesn't terminate type checking the following program.

The problem appears to arise from using the bound variable n which has type [ε]{Unit} as an argument to the constructor S.

on : {X -> {X -> Y} -> Y}
on x f = f x

interface Trivial = triv : Unit

data S = S { Unit }

interface State = get : S | put : S -> Unit

handleTrivial : <Trivial>X -> [State]X
handleTrivial x = x
handleTrivial <triv -> k> =
  on get! { (S n) -> put (S n); handleTrivial (k unit) }


main : { [Console]Unit }
main! = unit

[mpickering]

The problem is that the compiler tries to unify
MkDTTy "S" [EArg (MkAb (MkAbFVar "\163$f6") (fromList []))]
and MkDTTy "S" [EArg (MkAb (MkAbFVar "\163$f7") (fromList []))].

This falls into the second case of unifyAb' which creates a new unification variable but loops back to the same place in the call for solveForEVar.

If I reorder the clauses in solveAb' so that the last two cases for where one set of abilities is contained within the other are checked first then the compiler no longer loops.

[lucques]

Hi Matthew, just realised this problem is solved and must have been caused by a bug which has been fixed previously (in my branch-to-be-pulled-in-soon). I added your example as a regression test: c4532c6
Cheers, Lukas