Type checker loops with type families,
overlapping and undecidable instances
Manuel M T Chakravarty
chak at cse.unsw.edu.au
Sun Dec 7 19:51:34 EST 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-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
More information about the Glasgow-haskell-users
mailing list