Type checker loops with type families, overlapping and undecidable instances

Tom Schrijvers Tom.Schrijvers at cs.kuleuven.be
Thu Dec 4 09:19:02 EST 2008

>> -- Uncommenting the line below causes the typechecker to loop (GHC 6.10.1,
>> Windows)
>> --test = f Zero
> Is this expected behavior or a bug?

The call f Zero requires a co-inductive proof of the type class 
constraint (F Nat):

 	F Nat <=> Vieweable Nat /\ F' (View Nat)
 	      <=> True /\ F' (Unit :+: Nat)
 	      <=> True /\ F Unit /\ F Nat
 	      <=> True /\ True /\ F Nat

The type checker does have functionality for such co-inductive proof 
(generating co-inductive dictionaries), but apparently it's not kicking in 
here. Probably because of the separate fixedpoint loops for type classes 
and type families in the checker.

Tom Schrijvers

Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee

tel: +32 16 327544
e-mail: tom.schrijvers at cs.kuleuven.be
url: http://www.cs.kuleuven.be/~toms/

More information about the Glasgow-haskell-users mailing list