GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-08-30T12:55:21Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/15577TypeApplications-related infinite loop (GHC 8.6+ only)2019-08-30T12:55:21ZRyan ScottTypeApplications-related infinite loop (GHC 8.6+ only)The following program will loop infinitely when compiled on GHC 8.6 or HEAD:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Ty...The following program will loop infinitely when compiled on GHC 8.6 or HEAD:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
import Data.Type.Equality
data family Sing :: forall k. k -> Type
class Generic1 (f :: k -> Type) where
type Rep1 f :: k -> Type
class PGeneric1 (f :: k -> Type) where
type From1 (z :: f a) :: Rep1 f a
type To1 (z :: Rep1 f a) :: f a
class SGeneric1 (f :: k -> Type) where
sFrom1 :: forall (a :: k) (z :: f a). Sing z -> Sing (From1 z)
sTo1 :: forall (a :: k) (r :: Rep1 f a). Sing r -> Sing (To1 r :: f a)
class (PGeneric1 f, SGeneric1 f) => VGeneric1 (f :: k -> Type) where
sTof1 :: forall (a :: k) (z :: f a). Sing z -> To1 (From1 z) :~: z
sFot1 :: forall (a :: k) (r :: Rep1 f a). Sing r -> From1 (To1 r :: f a) :~: r
foo :: forall (f :: Type -> Type) (a :: Type) (r :: Rep1 f a).
VGeneric1 f
=> Sing r -> From1 (To1 r :: f a) :~: r
foo x
| Refl <- sFot1 -- Uncommenting the line below makes it work again:
-- @Type
@f @a @r x
= Refl
```
This is a regression from GHC 8.4, since compiling this program with 8.4 simply errors:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:35:20: error:
• Expecting one more argument to ‘f’
Expected a type, but ‘f’ has kind ‘* -> *’
• In the type ‘f’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl <- sFot1 @f @a @r x
In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl
|
35 | @f @a @r x
| ^
Bug.hs:35:23: error:
• Expected kind ‘f1 -> *’, but ‘a’ has kind ‘*’
• In the type ‘a’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl <- sFot1 @f @a @r x
In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)
|
35 | @f @a @r x
| ^
Bug.hs:35:26: error:
• Couldn't match kind ‘* -> *’ with ‘*’
When matching kinds
f1 :: * -> *
Rep1 f1 a1 :: *
Expected kind ‘f1’, but ‘r’ has kind ‘Rep1 f1 a1’
• In the type ‘r’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl <- sFot1 @f @a @r x
In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)
|
35 | @f @a @r x
| ^
Bug.hs:35:28: error:
• Couldn't match kind ‘*’ with ‘GHC.Types.RuntimeRep’
When matching kinds
a1 :: *
'GHC.Types.LiftedRep :: GHC.Types.RuntimeRep
• In the fourth argument of ‘sFot1’, namely ‘x’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl <- sFot1 @f @a @r x
In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)
|
35 | @f @a @r x
| ^
Bug.hs:36:5: error:
• Could not deduce: From1 (To1 r1) ~ r1
from the context: r0 ~ From1 (To1 r0)
bound by a pattern with constructor:
Refl :: forall k (a :: k). a :~: a,
in a pattern binding in
pattern guard for
an equation for ‘foo’
at Bug.hs:33:5-8
‘r1’ is a rigid type variable bound by
the type signature for:
foo :: forall (f1 :: * -> *) a1 (r1 :: Rep1 f1 a1).
VGeneric1 f1 =>
Sing r1 -> From1 (To1 r1) :~: r1
at Bug.hs:(29,1)-(31,43)
Expected type: From1 (To1 r1) :~: r1
Actual type: r1 :~: r1
• In the expression: Refl
In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)
|
36 | = Refl
| ^^^^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.5 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"TypeApplications-related infinite loop (GHC 8.6+ only)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeApplications,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program will loop infinitely when compiled on GHC 8.6 or HEAD:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE AllowAmbiguousTypes #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeApplications #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\n\r\ndata family Sing :: forall k. k -> Type\r\n\r\nclass Generic1 (f :: k -> Type) where\r\n type Rep1 f :: k -> Type\r\n\r\nclass PGeneric1 (f :: k -> Type) where\r\n type From1 (z :: f a) :: Rep1 f a\r\n type To1 (z :: Rep1 f a) :: f a\r\n\r\nclass SGeneric1 (f :: k -> Type) where\r\n sFrom1 :: forall (a :: k) (z :: f a). Sing z -> Sing (From1 z)\r\n sTo1 :: forall (a :: k) (r :: Rep1 f a). Sing r -> Sing (To1 r :: f a)\r\n\r\nclass (PGeneric1 f, SGeneric1 f) => VGeneric1 (f :: k -> Type) where\r\n sTof1 :: forall (a :: k) (z :: f a). Sing z -> To1 (From1 z) :~: z\r\n sFot1 :: forall (a :: k) (r :: Rep1 f a). Sing r -> From1 (To1 r :: f a) :~: r\r\n\r\nfoo :: forall (f :: Type -> Type) (a :: Type) (r :: Rep1 f a).\r\n VGeneric1 f\r\n => Sing r -> From1 (To1 r :: f a) :~: r\r\nfoo x\r\n | Refl <- sFot1 -- Uncommenting the line below makes it work again:\r\n -- @Type\r\n @f @a @r x\r\n = Refl\r\n}}}\r\n\r\nThis is a regression from GHC 8.4, since compiling this program with 8.4 simply errors:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:35:20: error:\r\n • Expecting one more argument to ‘f’\r\n Expected a type, but ‘f’ has kind ‘* -> *’\r\n • In the type ‘f’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl <- sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl\r\n |\r\n35 | @f @a @r x\r\n | ^\r\n\r\nBug.hs:35:23: error:\r\n • Expected kind ‘f1 -> *’, but ‘a’ has kind ‘*’\r\n • In the type ‘a’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl <- sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n |\r\n35 | @f @a @r x\r\n | ^\r\n\r\nBug.hs:35:26: error:\r\n • Couldn't match kind ‘* -> *’ with ‘*’\r\n When matching kinds\r\n f1 :: * -> *\r\n Rep1 f1 a1 :: *\r\n Expected kind ‘f1’, but ‘r’ has kind ‘Rep1 f1 a1’\r\n • In the type ‘r’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl <- sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n |\r\n35 | @f @a @r x\r\n | ^\r\n\r\nBug.hs:35:28: error:\r\n • Couldn't match kind ‘*’ with ‘GHC.Types.RuntimeRep’\r\n When matching kinds\r\n a1 :: *\r\n 'GHC.Types.LiftedRep :: GHC.Types.RuntimeRep\r\n • In the fourth argument of ‘sFot1’, namely ‘x’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl <- sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n |\r\n35 | @f @a @r x\r\n | ^\r\n\r\nBug.hs:36:5: error:\r\n • Could not deduce: From1 (To1 r1) ~ r1\r\n from the context: r0 ~ From1 (To1 r0)\r\n bound by a pattern with constructor:\r\n Refl :: forall k (a :: k). a :~: a,\r\n in a pattern binding in\r\n pattern guard for\r\n an equation for ‘foo’\r\n at Bug.hs:33:5-8\r\n ‘r1’ is a rigid type variable bound by\r\n the type signature for:\r\n foo :: forall (f1 :: * -> *) a1 (r1 :: Rep1 f1 a1).\r\n VGeneric1 f1 =>\r\n Sing r1 -> From1 (To1 r1) :~: r1\r\n at Bug.hs:(29,1)-(31,43)\r\n Expected type: From1 (To1 r1) :~: r1\r\n Actual type: r1 :~: r1\r\n • In the expression: Refl\r\n In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n |\r\n36 | = Refl\r\n | ^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.8.2Ben GamariAlp MestanogullariBen Gamari