Re: Type checker loops with type families, overlapping and undecidable instances

8 Dec 2008

      ...
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-extension...),
"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 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 :
...
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

Re: Type checker loops with type families, overlapping and undecidable instances

Martin Sulzmann