Type checker loops with type families, overlapping and undecidable instances

[Martin Sulzmann]

> The interaction between solving class constraints and equalities with type
> families is currently rather ad hoc.
>

FYI

*September 2008*
*Unified Type Checking for Type Classes and Type Families*, T. Schrijvers,
M. Sulzmann. Presented at the ICFP 2008 poster session
(pdf available on Tom's homepage).

We propose to encode type class solving as type function solving. Earlier, I
suggested
the opposite direction. Either way works and leads to a system which can
properly
deal with any sort of type class and type function interaction plus can be
straightforwardly extended to support co-inductive type classes/functions.

-Martin

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
>
>
>
> _______________________________________________
> 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/00d85ef2/attachment-0001.htm