Type checker loops with type families, overlapping and undecidable instances

[Tom Schrijvers]

>> -- 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
Belgium

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