Re: Type checker loops with type families, overlapping and undecidable instances

2008-12-08 Thread Martin Sulzmann
> The interaction between solving class constraints and equalities with type > families is currently rather ad hoc. > FYI *September 2008* *Unified Type Checking for Type Classes and Type Families*, T. Schrijvers, M. Sulzmann. Presented at the ICFP 2008 poster session (pdf available on Tom's home

Re: Type checker loops with type families, overlapping and undecidable instances

2008-12-07 Thread Manuel M T Chakravarty
As Lennart wrote, with UndecideableInstances all bets are off. Concerning the fixed-depth recursion stack. It is currently only used for the simplification of class instance declarations, but if improvement rules are involved (either FDs or TFs) that check will not catch all cases anyway.

Re: Type checker loops with type families, overlapping and undecidable instances

2008-12-04 Thread 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

Re: Type checker loops with type families, overlapping and undecidable instances

2008-12-04 Thread José Pedro Magalhães
Hello Lennart, Yes, but according to the manual ( http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class-extensions.html#undecidable-instances), "Termination is ensured by having a fixed-depth recursion stack". So I would expect at least termination, which I'm not getting (but I guess

Re: Type checker loops with type families, overlapping and undecidable instances

2008-12-04 Thread Lennart Augustsson
Turning on UndecidableInstances is the same as saying: OK typechcker, you can loop if I make a mistake. I've not looked closely at your code, but if you turn on that flag, looping is probably not a bug. -- Lennart 2008/12/4 José Pedro Magalhães <[EMAIL PROTECTED]>: > Hello all, > > Please consi

Type checker loops with type families, overlapping and undecidable instances

2008-12-04 Thread José Pedro Magalhães
Hello all, Please consider the following code: {-# OPTIONS -Wall #-} > {-# LANGUAGE FlexibleContexts #-} > {-# LANGUAGE FlexibleInstances#-} > {-# LANGUAGE TypeOperators#-} > {-# LANGUAGE TypeFamilies #-} > {-# LANGUAGE OverlappingInstances #-} > {-# LANGUA