Type check loop on impredicativaty + GADT mix
The type checker runs out of stack space on checking compose
, but not compose'
or composeS
{-# OPTIONS_GHC -fglasgow-exts #-}
module Compose where
data Z
data S n
data List n a where
Nil :: List Z a
(:-) :: a -> List n a -> List (S n) a
data Hold a = Hold (forall m . a m -> a (S m))
compose' :: List n (Hold a) -> a (S Z) -> a (S n)
compose' Nil x = x
compose' ((Hold f) :- fs) x = f (compose' fs x)
compose :: List n (forall m . a m -> a (S m)) -> a (S Z) -> a (S n)
compose Nil x = x
compose (f :- fs) x = f (compose fs x)
composeS :: [forall m . a m -> a m] -> a n -> a n
composeS [] x = x
composeS (f:fs) x = f (composeS fs x)
Trac metadata
Trac field | Value |
---|---|
Version | 6.6 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |