Type checker loops with type families, overlapping and undecidable instances

[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.

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-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 that can be due to the type families).
>
>
> Thanks,
> Pedro
>
> On Thu, Dec 4, 2008 at 15:10, Lennart Augustsson <lennart at augustsson.net 
> > 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 <jpm at cs.uu.nl>:
> > 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 at haskell.org
> > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
> >
> >
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20081208/7b9df5cc/attachment.htm