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@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@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@haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users