id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc,os,architecture,failure,difficulty,testcase,blockedby,blocking,related
4093,compiler hangs (type checking?),dias,simonpj,"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
}}}",bug,closed,high,7.0.1,Compiler,6.13,fixed,,,Linux,x86,Compile-time crash,,"indexed-types/should_fail/T4093a, T4093b",,,