compiler hangs (type checking?)

[dias]

The compiler hangs while compiling the following program, probably during type checking. Perhaps it has something to do with type functions?

Note: I can give you several variations of the same program that also hang. Let me know if you want them.

{-# LANGUAGE GADTs, EmptyDataDecls, ScopedTypeVariables, TypeFamilies #-}

module Test () where

data C
data O

type family   EitherCO e a b :: *
type instance EitherCO C a b = a
type instance EitherCO O a b = b

data MaybeC ex t where
  JustC    :: t -> MaybeC C t
  NothingC ::      MaybeC O t

data Block (n :: * -> * -> *) e x


blockToNodeList ::
  forall n e x. (EitherCO e (A C O n) (A O O n) ~ A e O n,
                 EitherCO x (A C C n) (A C O n) ~ A C x n) =>
    Block n e x -> A e x n

type A e x n = (MaybeC e (n C O), MaybeC x (n O C))
blockToNodeList b = foldBlockNodesF (f, l) b z 
  where
    z :: EitherCO e (EitherCO e (A C O n) (A O O n)) (EitherCO e (A C O n) (A O O n))
    z = undefined

    f :: n C O -> EitherCO e (A C O n) (A O O n) -> EitherCO e (A C O n) (A O O n)
    f n _ = (JustC n, NothingC)

    l :: n O C -> EitherCO e (A C O n) (A O O n) -> EitherCO e (A C C n) (A O C n)
    l _ = undefined

foldBlockNodesF  :: forall n a b c e x .
                   ( n C O       -> a -> b
                   , n O C       -> b -> c)
                 -> (Block n e x -> EitherCO e a b -> EitherCO x c b)
foldBlockNodesF _ = undefined

[cam]

The following code (with fewer extensions enabled) gives me the same result, and is presumably the same bug:

{-# LANGUAGE TypeFamilies #-}
module Test () where

type family Foo x
type instance Foo () = Maybe ()

hang :: (Foo e ~ Maybe e) => Foo e
hang = Just ()

The above, and the earlier code, both result in 100% CPU until GHC falls over with a stack overflow. Tested on GHC 6.10.4 (Linux and Windows), GHC 6.12.2 (Windows), and GHC 6.13.20100522 (Linux).

[simonpj]

Well that's definitely a bug! It should fail with something like "Can't unify e with ()".

I have a week blocked out in June to work on the new type inference engine, so I'm hoping you can work around this until then.

Simon

[dias]

I have a week blocked out in June to work on the new type inference engine, so I'm hoping you can work around this until then.

June sounds good. I was just trying to find a "simple" way to write the block->list function in Hoopl, while building my intuition for how type functions work.

[simonpj]

This is indeed fixed with the new typechecker.

Can you try in your application? Use the HEAD, or the upcoming release candidate.

I'm pretty confident it's fixed, so I'll close it meanwhile.

Simon