GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T19:15:11Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/1118Type check loop on impredicativaty + GADT mix2019-07-07T19:15:11ZjappleType check loop on impredicativaty + GADT mixThe 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)
```
<details><summary>Trac metadata</summary>
| 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 | |
</details>
<!-- {"blocked_by":[],"summary":"Type check loop on impredicativaty + GADT mix","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.6","keywords":["GADTs","impredicativity,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The type checker runs out of stack space on checking {{{compose}}}, but not {{{compose'}}} or {{{composeS}}}\r\n\r\n{{{\r\n{-# OPTIONS_GHC -fglasgow-exts #-}\r\n\r\nmodule Compose where\r\n\r\ndata Z\r\ndata S n\r\n\r\ndata List n a where\r\n Nil :: List Z a\r\n (:-) :: a -> List n a -> List (S n) a\r\n\r\ndata Hold a = Hold (forall m . a m -> a (S m))\r\n\r\ncompose' :: List n (Hold a) -> a (S Z) -> a (S n)\r\ncompose' Nil x = x\r\ncompose' ((Hold f) :- fs) x = f (compose' fs x)\r\n\r\ncompose :: List n (forall m . a m -> a (S m)) -> a (S Z) -> a (S n)\r\ncompose Nil x = x\r\ncompose (f :- fs) x = f (compose fs x)\r\n\r\ncomposeS :: [forall m . a m -> a m] -> a n -> a n\r\ncomposeS [] x = x\r\ncomposeS (f:fs) x = f (composeS fs x)\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->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)
```
<details><summary>Trac metadata</summary>
| 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 | |
</details>
<!-- {"blocked_by":[],"summary":"Type check loop on impredicativaty + GADT mix","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.6","keywords":["GADTs","impredicativity,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The type checker runs out of stack space on checking {{{compose}}}, but not {{{compose'}}} or {{{composeS}}}\r\n\r\n{{{\r\n{-# OPTIONS_GHC -fglasgow-exts #-}\r\n\r\nmodule Compose where\r\n\r\ndata Z\r\ndata S n\r\n\r\ndata List n a where\r\n Nil :: List Z a\r\n (:-) :: a -> List n a -> List (S n) a\r\n\r\ndata Hold a = Hold (forall m . a m -> a (S m))\r\n\r\ncompose' :: List n (Hold a) -> a (S Z) -> a (S n)\r\ncompose' Nil x = x\r\ncompose' ((Hold f) :- fs) x = f (compose' fs x)\r\n\r\ncompose :: List n (forall m . a m -> a (S m)) -> a (S Z) -> a (S n)\r\ncompose Nil x = x\r\ncompose (f :- fs) x = f (compose fs x)\r\n\r\ncomposeS :: [forall m . a m -> a m] -> a n -> a n\r\ncomposeS [] x = x\r\ncomposeS (f:fs) x = f (composeS fs x)\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->6.6.1Simon Peyton JonesSimon Peyton Jones