Type checker loops with type families, overlapping and undecidable instances

[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
> >
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20081204/46b909c1/attachment.htm