Type checker loops with type families,
overlapping and undecidable instances
José Pedro Magalhães
jpm at cs.uu.nl
Thu Dec 4 09:13:37 EST 2008
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
> >
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20081204/46b909c1/attachment.htm
More information about the Glasgow-haskell-users
mailing list