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

7 Dec 2008

      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.

The interaction between solving class constraints and equalities with  
type families is currently rather ad hoc.  We are currently re- 
designing that interaction and may then make the fixed-depth  
restriction more broadly applicable.  However, as Tom already  
mentioned, the cycle does not involve type families in your example  
anyway.

Manuel

José Pedro Magalhães:
...
Hello Lennart,
Yes, but according to the manual (http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class-extension... 
), "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 that can be due to the type families).
Thanks,
Pedro
On Thu, Dec 4, 2008 at 15:10, Lennart Augustsson 
...
wrote:
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 :
...
Hello all,
Please consider the following code:
...
{-# OPTIONS -Wall                 #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE UndecidableInstances #-}
module Test where
-- Some view
class Viewable a where
  type View a
  to   :: a -> View a
-- Structural representations
data Unit    = Unit
data a :+: b = L a | R b
instance Viewable Unit where
  type View Unit = Unit
  to = id
instance (Viewable a, Viewable b) => Viewable (a :+: b) where
  type View (a :+: b) = a :+: b
  to = id
-- Worker class
class F' a where
  f' :: a -> ()
instance F' Unit where
  f' Unit = ()
instance (F a, F b) => F' (a :+: b) where
  f' (L x) = f x
  f' (R x) = f x
-- Dispatcher class
class (Viewable a, F' (View a)) => F a where
  f :: a -> ()
  f = f' . to
instance F Unit where
  f = f'
instance (F a, F b) => F (a :+: b) where
  f = f'
-- All generic instances
instance (Viewable a, F' (View a)) => F a
-- A recursive datatype
data Nat = Zero | Succ Nat
-- Instance of Viewable
instance Viewable Nat where
  type View Nat = Unit :+: Nat
  to = undefined
-- Uncommenting the line below causes the typechecker to loop  
(GHC 6.10.1,
Windows)
--test = f Zero
Is this expected behavior or a bug?
Thanks,
Pedro
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

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

Manuel M T Chakravarty