Type checker hangs

[MartijnVanSteenbergen]

The following module causes ghc --make and ghci to hang. -ddump-tc-trace produces output indefinitely.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleContexts #-}

import Generics.MultiRec
import Control.Monad.Writer

data AnyF s f where
  AnyF :: s ix -> f ix -> AnyF s f

children :: HFunctor s (PF s) => s ix -> (PF s) r ix -> [AnyF s r]
children p x = execWriter (hmapM p collect x) where
  collect :: (HFunctor s (PF s)) => s ix -> r ix -> Writer [AnyF s r] (r ix)
  collect w x = tell [AnyF w x] >> return x

Module Generics.MultiRec is from Hackage package multirec-0.4.

The code contains a type error: if arguments p and collect are swapped the code compiles fine.

I haven't tried making this example any smaller.

[MartijnVanSteenbergen]

Reproducible in GHC 6.10.3.

[chak]

Would you mind trying with the current development version? There have been significant changes to the type checker (and I haven't got multirec handy).

[MartijnVanSteenbergen]

I'm afraid that will take me a significant amount of time. :-(

What I've done instead is change the example to be independent of multirec, moving some definitions into the snippet. I've also tried to make it smaller, removing some function arguments, type arguments and class constraints and replacing definitions by undefined. In what is left I cannot find anything else I can remove without causing GHC not to hang anymore.

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}

import Control.Monad.Writer

data AnyF (s :: * -> *) = AnyF
class HFunctor (f :: (* -> *) -> * -> *)
type family PF (phi :: * -> *) :: (* -> *) -> * -> *

children :: s ix -> (PF s) r ix -> [AnyF s]
children p x = execWriter (hmapM p collect x)

collect :: HFunctor (PF s) => s ix -> r ix -> Writer [AnyF s] (r ix)
collect = undefined

hmapM :: (forall ix. phi ix -> r ix -> m (r' ix))
  -> phi ix -> f r ix -> m (f r' ix)
hmapM = undefined

Does that help?

[simonpj]

That's much easier, thank you v much.

Simon

[EduardSergeev]

output from GHC with -ddump-tc-trace

[EduardSergeev]

I think I am now facing a similar behavior (hangs while compiling, continiously consuming memory until the whole system hangs) from GHC 6.10.3 on Mac OS X 10.5.7 (and on Windows XP as well) on the following simple type family example:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}

class RFunctor c a b where
    type Res c a b :: *
    rmap :: (a -> b) -> c -> Res c a b

instance (a ~ c) => RFunctor c a b where
    type Res c a b = b
    rmap f = f

instance (RFunctor c a b, a ~ c) => RFunctor [c] a b where
    type Res [c] a b = [b]
    rmap f = map (map f)

But if these two instances declarations are interchanged it reports:

Conflicting family instance declarations:

type instance Res [c] a b -- Defined at TFTest.hs:14:9-11 type instance Res c a b -- Defined at TFTest.hs:18:9-11

I've also attached the fragment of the output from GHC with -ddump-tc-trace

[byorgey]

I think I've also tickled this bug, which appears to still exist in 6.12.1rc2. Here's a stripped-down version of the code that causes GHC to diverge for me:

{-# LANGUAGE EmptyDataDecls, TypeFamilies, TypeOperators, GADTs, KindSignatures #-}

data (f :+: g) x = Inl (f x) | Inr (g x)

data R :: (* -> *) -> * where
  RSum  :: R f -> R g -> R (f :+: g)

class Rep f where
  rep :: R f

instance (Rep f, Rep g) => Rep (f :+: g) where
  rep = RSum rep rep

type family Der (f :: * -> *) :: * -> *
type instance Der (f :+: g) = Der f :+: Der g

plug :: Rep f => Der f x -> x -> f x
plug = plug' rep where
  plug' :: R f -> Der f x -> x -> f x
  plug' (RSum rf rg) (Inl df) x = Inl (plug rf df x)

Note that this code has a bug; the call to plug in the last line ought to be plug' (and it works properly when fixed), but I would expect a type error instead of a diverging compiler.

I'm classifying this as a "compile-time crash" since one bottom is as good as another. ;)

[simonpj]

Thanks for another very useful test case. I think it's going to have to wait for the glorious new constraint checker that Dimitrios and I are slowly (but actively) working on.

Simon