Type checker loops with type families, overlapping and undecidable instances

4 Dec 2008

      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

Type checker loops with type families, overlapping and undecidable instances

José Pedro Magalhães