GHC issueshttps://gitlab.haskell.org/ghc/ghc/issues20190707T18:20:12Zhttps://gitlab.haskell.org/ghc/ghc/issues/13761Can't create polykinded GADT with TypeInType enabled, but can without20190707T18:20:12ZRyan ScottCan't create polykinded GADT with TypeInType enabled, but can withoutSurprisingly, this compiles without `TypeInType`:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE PolyKinds #}
module Works where
import Data.Kind
data T :: k > Type where
MkT :: T Int
```
But once you add `TypeInType`:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
data T :: k > Type where
MkT :: T Int
```
then it stops working!
```
GHCi, version 8.3.20170516: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:11:12: error:
• Expected kind ‘k’, but ‘Int’ has kind ‘*’
• In the first argument of ‘T’, namely ‘Int’
In the type ‘T Int’
In the definition of data constructor ‘MkT’

11  MkT :: T Int
 ^^^
```
This bug is present in GHC 8.0.1, 8.0.2, 8.2.1, and HEAD.
What's strange about this bug is that is requires that you write `T` with an explicit kind signature. If you write `T` like this:
```hs
data T (a :: k) where
MkT :: T Int
```
Then it will work with `TypeInType` enabled.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Can't create polykinded GADT with TypeInType enabled, but can without","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Surprisingly, this compiles without `TypeInType`:\r\n\r\n{{{#!hs\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE KindSignatures #}\r\n{# LANGUAGE PolyKinds #}\r\nmodule Works where\r\n\r\nimport Data.Kind\r\n\r\ndata T :: k > Type where\r\n MkT :: T Int\r\n}}}\r\n\r\nBut once you add `TypeInType`:\r\n\r\n{{{#!hs\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE KindSignatures #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE TypeInType #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata T :: k > Type where\r\n MkT :: T Int\r\n}}}\r\n\r\nthen it stops working!\r\n\r\n{{{\r\nGHCi, version 8.3.20170516: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:11:12: error:\r\n • Expected kind ‘k’, but ‘Int’ has kind ‘*’\r\n • In the first argument of ‘T’, namely ‘Int’\r\n In the type ‘T Int’\r\n In the definition of data constructor ‘MkT’\r\n \r\n11  MkT :: T Int\r\n  ^^^\r\n}}}\r\n\r\nThis bug is present in GHC 8.0.1, 8.0.2, 8.2.1, and HEAD.\r\n\r\nWhat's strange about this bug is that is requires that you write `T` with an explicit kind signature. If you write `T` like this:\r\n\r\n{{{#!hs\r\ndata T (a :: k) where\r\n MkT :: T Int\r\n}}}\r\n\r\nThen it will work with `TypeInType` enabled.","type_of_failure":"OtherFailure","blocking":[]} >Surprisingly, this compiles without `TypeInType`:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE PolyKinds #}
module Works where
import Data.Kind
data T :: k > Type where
MkT :: T Int
```
But once you add `TypeInType`:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
data T :: k > Type where
MkT :: T Int
```
then it stops working!
```
GHCi, version 8.3.20170516: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:11:12: error:
• Expected kind ‘k’, but ‘Int’ has kind ‘*’
• In the first argument of ‘T’, namely ‘Int’
In the type ‘T Int’
In the definition of data constructor ‘MkT’

11  MkT :: T Int
 ^^^
```
This bug is present in GHC 8.0.1, 8.0.2, 8.2.1, and HEAD.
What's strange about this bug is that is requires that you write `T` with an explicit kind signature. If you write `T` like this:
```hs
data T (a :: k) where
MkT :: T Int
```
Then it will work with `TypeInType` enabled.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Can't create polykinded GADT with TypeInType enabled, but can without","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Surprisingly, this compiles without `TypeInType`:\r\n\r\n{{{#!hs\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE KindSignatures #}\r\n{# LANGUAGE PolyKinds #}\r\nmodule Works where\r\n\r\nimport Data.Kind\r\n\r\ndata T :: k > Type where\r\n MkT :: T Int\r\n}}}\r\n\r\nBut once you add `TypeInType`:\r\n\r\n{{{#!hs\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE KindSignatures #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE TypeInType #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata T :: k > Type where\r\n MkT :: T Int\r\n}}}\r\n\r\nthen it stops working!\r\n\r\n{{{\r\nGHCi, version 8.3.20170516: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:11:12: error:\r\n • Expected kind ‘k’, but ‘Int’ has kind ‘*’\r\n • In the first argument of ‘T’, namely ‘Int’\r\n In the type ‘T Int’\r\n In the definition of data constructor ‘MkT’\r\n \r\n11  MkT :: T Int\r\n  ^^^\r\n}}}\r\n\r\nThis bug is present in GHC 8.0.1, 8.0.2, 8.2.1, and HEAD.\r\n\r\nWhat's strange about this bug is that is requires that you write `T` with an explicit kind signature. If you write `T` like this:\r\n\r\n{{{#!hs\r\ndata T (a :: k) where\r\n MkT :: T Int\r\n}}}\r\n\r\nThen it will work with `TypeInType` enabled.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc/issues/13674Poor error message which masks occurscheck failure20190707T18:20:39ZRyan ScottPoor error message which masks occurscheck failureHere's some code, reduced from an example in https://github.com/ekmett/constraints/issues/55:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
import Data.Proxy
import GHC.Exts (Constraint)
import GHC.TypeLits
import Unsafe.Coerce (unsafeCoerce)
data Dict :: Constraint > * where
Dict :: a => Dict a
infixr 9 :
newtype a : b = Sub (a => Dict b)
  Given that @a : b@, derive something that needs a context @b@, using the context @a@
(\\) :: a => (b => r) > (a : b) > r
r \\ Sub Dict = r
newtype Magic n = Magic (KnownNat n => Dict (KnownNat n))
magic :: forall n m o. (Integer > Integer > Integer) > (KnownNat n, KnownNat m) : KnownNat o
magic f = Sub $ unsafeCoerce (Magic Dict) (natVal (Proxy :: Proxy n) `f` natVal (Proxy :: Proxy m))
type family Lcm :: Nat > Nat > Nat where
axiom :: forall a b. Dict (a ~ b)
axiom = unsafeCoerce (Dict :: Dict (a ~ a))
lcmNat :: forall n m. (KnownNat n, KnownNat m) : KnownNat (Lcm n m)
lcmNat = magic lcm
lcmIsIdempotent :: forall n. Dict (n ~ Lcm n n)
lcmIsIdempotent = axiom
newtype GF (n :: Nat) = GF Integer
instance KnownNat n => Num (GF n) where
xf@(GF x) + GF y = GF $ (x+y) `mod` (natVal xf)
xf@(GF x)  GF y = GF $ (xy) `mod` (natVal xf)
xf@(GF x) * GF y = GF $ (x*y) `mod` (natVal xf)
abs = id
signum xf@(GF x)  x==0 = xf
 otherwise = GF 1
fromInteger = GF
x :: GF 5
x = GF 3
y :: GF 5
y = GF 4
foo :: (KnownNat m, KnownNat n) => GF m > GF n > GF (Lcm m n)
foo m@(GF x) n@(GF y) = GF $ (x*y) `mod` (lcm (natVal m) (natVal n))
bar :: (KnownNat m) => GF m > GF m > GF m
bar (x :: GF m) y = foo x y  foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
```
Compiling this (with either GHC 8.0.1, 8.0.2, 8.2.1, or HEAD) gives you a downright puzzling type error:
```
$ /opt/ghc/head/bin/ghci Bug.hs
GHCi, version 8.3.20170509: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:63:21: error:
• Couldn't match type ‘m’ with ‘Lcm m m’
‘m’ is a rigid type variable bound by
the type signature for:
bar :: forall (m :: Nat). KnownNat m => GF m > GF m > GF m
at Bug.hs:62:144
Expected type: GF m
Actual type: GF (Lcm m m)
• In the first argument of ‘()’, namely ‘foo x y’
In the expression:
foo x y  foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
In an equation for ‘bar’:
bar (x :: GF m) y
= foo x y  foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
• Relevant bindings include
y :: GF m (bound at Bug.hs:63:17)
x :: GF m (bound at Bug.hs:63:6)
bar :: GF m > GF m > GF m (bound at Bug.hs:63:1)

63  bar (x :: GF m) y = foo x y  foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
 ^^^^^^^
Bug.hs:63:31: error:
• Could not deduce: m ~ Lcm m m
from the context: m ~ Lcm m m
bound by a type expected by the context:
m ~ Lcm m m => GF m
at Bug.hs:63:3185
‘m’ is a rigid type variable bound by
the type signature for:
bar :: forall (m :: Nat). KnownNat m => GF m > GF m > GF m
at Bug.hs:62:144
Expected type: GF m
Actual type: GF (Lcm m m)
• In the first argument of ‘(\\)’, namely ‘foo y x’
In the first argument of ‘(\\)’, namely ‘foo y x \\ lcmNat @m @m’
In the second argument of ‘()’, namely
‘foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)’
• Relevant bindings include
y :: GF m (bound at Bug.hs:63:17)
x :: GF m (bound at Bug.hs:63:6)
bar :: GF m > GF m > GF m (bound at Bug.hs:63:1)

63  bar (x :: GF m) y = foo x y  foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
 ^^^^^^^
```
In particular, I'd like to emphasize this part:
```
• Could not deduce: m ~ Lcm m m
from the context: m ~ Lcm m m
```
Wat!? Surely, GHC can deduce `m ~ Lcm m m` from `m ~ Lcm m m`? I decided to flip on `fprintexplicitkinds` and see if there was some other issue lurking beneath the surface:
```
$ /opt/ghc/head/bin/ghci Bug.hs fprintexplicitkinds
GHCi, version 8.3.20170509: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:63:21: error:
• Couldn't match type ‘m’ with ‘Lcm m m’
‘m’ is a rigid type variable bound by
the type signature for:
bar :: forall (m :: Nat). KnownNat m => GF m > GF m > GF m
at Bug.hs:62:144
Expected type: GF m
Actual type: GF (Lcm m m)
• In the first argument of ‘()’, namely ‘foo x y’
In the expression:
foo x y  foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
In an equation for ‘bar’:
bar (x :: GF m) y
= foo x y  foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
• Relevant bindings include
y :: GF m (bound at Bug.hs:63:17)
x :: GF m (bound at Bug.hs:63:6)
bar :: GF m > GF m > GF m (bound at Bug.hs:63:1)

63  bar (x :: GF m) y = foo x y  foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
 ^^^^^^^
Bug.hs:63:31: error:
• Could not deduce: (m :: Nat) ~~ (Lcm m m :: Nat)
from the context: m ~ Lcm m m
bound by a type expected by the context:
m ~ Lcm m m => GF m
at Bug.hs:63:3185
‘m’ is a rigid type variable bound by
the type signature for:
bar :: forall (m :: Nat). KnownNat m => GF m > GF m > GF m
at Bug.hs:62:144
Expected type: GF m
Actual type: GF (Lcm m m)
• In the first argument of ‘(\\)’, namely ‘foo y x’
In the first argument of ‘(\\)’, namely ‘foo y x \\ lcmNat @m @m’
In the second argument of ‘()’, namely
‘foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)’
• Relevant bindings include
y :: GF m (bound at Bug.hs:63:17)
x :: GF m (bound at Bug.hs:63:6)
bar :: GF m > GF m > GF m (bound at Bug.hs:63:1)

63  bar (x :: GF m) y = foo x y  foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)

```
Well, not a whole lot changed. We now have this, slightly more specific error instead:
```
• Could not deduce: (m :: Nat) ~~ (Lcm m m :: Nat)
from the context: m ~ Lcm m m
```
Huh, this is flummoxing. Surely `(m :: Nat) ~~ (Lcm m m :: Nat)` ought to be the same thing as `m ~ Lcm m m`, right?Here's some code, reduced from an example in https://github.com/ekmett/constraints/issues/55:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
import Data.Proxy
import GHC.Exts (Constraint)
import GHC.TypeLits
import Unsafe.Coerce (unsafeCoerce)
data Dict :: Constraint > * where
Dict :: a => Dict a
infixr 9 :
newtype a : b = Sub (a => Dict b)
  Given that @a : b@, derive something that needs a context @b@, using the context @a@
(\\) :: a => (b => r) > (a : b) > r
r \\ Sub Dict = r
newtype Magic n = Magic (KnownNat n => Dict (KnownNat n))
magic :: forall n m o. (Integer > Integer > Integer) > (KnownNat n, KnownNat m) : KnownNat o
magic f = Sub $ unsafeCoerce (Magic Dict) (natVal (Proxy :: Proxy n) `f` natVal (Proxy :: Proxy m))
type family Lcm :: Nat > Nat > Nat where
axiom :: forall a b. Dict (a ~ b)
axiom = unsafeCoerce (Dict :: Dict (a ~ a))
lcmNat :: forall n m. (KnownNat n, KnownNat m) : KnownNat (Lcm n m)
lcmNat = magic lcm
lcmIsIdempotent :: forall n. Dict (n ~ Lcm n n)
lcmIsIdempotent = axiom
newtype GF (n :: Nat) = GF Integer
instance KnownNat n => Num (GF n) where
xf@(GF x) + GF y = GF $ (x+y) `mod` (natVal xf)
xf@(GF x)  GF y = GF $ (xy) `mod` (natVal xf)
xf@(GF x) * GF y = GF $ (x*y) `mod` (natVal xf)
abs = id
signum xf@(GF x)  x==0 = xf
 otherwise = GF 1
fromInteger = GF
x :: GF 5
x = GF 3
y :: GF 5
y = GF 4
foo :: (KnownNat m, KnownNat n) => GF m > GF n > GF (Lcm m n)
foo m@(GF x) n@(GF y) = GF $ (x*y) `mod` (lcm (natVal m) (natVal n))
bar :: (KnownNat m) => GF m > GF m > GF m
bar (x :: GF m) y = foo x y  foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
```
Compiling this (with either GHC 8.0.1, 8.0.2, 8.2.1, or HEAD) gives you a downright puzzling type error:
```
$ /opt/ghc/head/bin/ghci Bug.hs
GHCi, version 8.3.20170509: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:63:21: error:
• Couldn't match type ‘m’ with ‘Lcm m m’
‘m’ is a rigid type variable bound by
the type signature for:
bar :: forall (m :: Nat). KnownNat m => GF m > GF m > GF m
at Bug.hs:62:144
Expected type: GF m
Actual type: GF (Lcm m m)
• In the first argument of ‘()’, namely ‘foo x y’
In the expression:
foo x y  foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
In an equation for ‘bar’:
bar (x :: GF m) y
= foo x y  foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
• Relevant bindings include
y :: GF m (bound at Bug.hs:63:17)
x :: GF m (bound at Bug.hs:63:6)
bar :: GF m > GF m > GF m (bound at Bug.hs:63:1)

63  bar (x :: GF m) y = foo x y  foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
 ^^^^^^^
Bug.hs:63:31: error:
• Could not deduce: m ~ Lcm m m
from the context: m ~ Lcm m m
bound by a type expected by the context:
m ~ Lcm m m => GF m
at Bug.hs:63:3185
‘m’ is a rigid type variable bound by
the type signature for:
bar :: forall (m :: Nat). KnownNat m => GF m > GF m > GF m
at Bug.hs:62:144
Expected type: GF m
Actual type: GF (Lcm m m)
• In the first argument of ‘(\\)’, namely ‘foo y x’
In the first argument of ‘(\\)’, namely ‘foo y x \\ lcmNat @m @m’
In the second argument of ‘()’, namely
‘foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)’
• Relevant bindings include
y :: GF m (bound at Bug.hs:63:17)
x :: GF m (bound at Bug.hs:63:6)
bar :: GF m > GF m > GF m (bound at Bug.hs:63:1)

63  bar (x :: GF m) y = foo x y  foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
 ^^^^^^^
```
In particular, I'd like to emphasize this part:
```
• Could not deduce: m ~ Lcm m m
from the context: m ~ Lcm m m
```
Wat!? Surely, GHC can deduce `m ~ Lcm m m` from `m ~ Lcm m m`? I decided to flip on `fprintexplicitkinds` and see if there was some other issue lurking beneath the surface:
```
$ /opt/ghc/head/bin/ghci Bug.hs fprintexplicitkinds
GHCi, version 8.3.20170509: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:63:21: error:
• Couldn't match type ‘m’ with ‘Lcm m m’
‘m’ is a rigid type variable bound by
the type signature for:
bar :: forall (m :: Nat). KnownNat m => GF m > GF m > GF m
at Bug.hs:62:144
Expected type: GF m
Actual type: GF (Lcm m m)
• In the first argument of ‘()’, namely ‘foo x y’
In the expression:
foo x y  foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
In an equation for ‘bar’:
bar (x :: GF m) y
= foo x y  foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
• Relevant bindings include
y :: GF m (bound at Bug.hs:63:17)
x :: GF m (bound at Bug.hs:63:6)
bar :: GF m > GF m > GF m (bound at Bug.hs:63:1)

63  bar (x :: GF m) y = foo x y  foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
 ^^^^^^^
Bug.hs:63:31: error:
• Could not deduce: (m :: Nat) ~~ (Lcm m m :: Nat)
from the context: m ~ Lcm m m
bound by a type expected by the context:
m ~ Lcm m m => GF m
at Bug.hs:63:3185
‘m’ is a rigid type variable bound by
the type signature for:
bar :: forall (m :: Nat). KnownNat m => GF m > GF m > GF m
at Bug.hs:62:144
Expected type: GF m
Actual type: GF (Lcm m m)
• In the first argument of ‘(\\)’, namely ‘foo y x’
In the first argument of ‘(\\)’, namely ‘foo y x \\ lcmNat @m @m’
In the second argument of ‘()’, namely
‘foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)’
• Relevant bindings include
y :: GF m (bound at Bug.hs:63:17)
x :: GF m (bound at Bug.hs:63:6)
bar :: GF m > GF m > GF m (bound at Bug.hs:63:1)

63  bar (x :: GF m) y = foo x y  foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)

```
Well, not a whole lot changed. We now have this, slightly more specific error instead:
```
• Could not deduce: (m :: Nat) ~~ (Lcm m m :: Nat)
from the context: m ~ Lcm m m
```
Huh, this is flummoxing. Surely `(m :: Nat) ~~ (Lcm m m :: Nat)` ought to be the same thing as `m ~ Lcm m m`, right?https://gitlab.haskell.org/ghc/ghc/issues/13650Implement KPush in types20190707T18:20:47ZRichard Eisenbergrae@richarde.devImplement KPush in typesA recent commit contributed a [Note](https://phabricator.haskell.org/diffusion/GHC/browse/master/compiler/types/Type.hs;a483e711da7834bc952367f554ac4e877b4e157a$1191) that explains why we need the dreaded KPush rule to be implemented in `splitTyConApp`. Without KPush there, it's possible that we can have two types t1 and t2 such that `t1 `eqType` t2` and yet they respond differently to `splitTyConApp`: t1 = `(T > co1) (a > co2)` and t2 = `T a`. Both t1 and t2 are wellkinded and can have the same kind. But one is a `TyConApp` and one is an `AppTy`. (Actually, looking at this, perhaps the magic will be in `mkAppTy`, not `splitTyConApp`.) But I have to look closer.
This ticket serves as a reminder to do so.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  
 Type  Task 
 TypeOfFailure  OtherFailure 
 Priority  high 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Implement KPush in types","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"A recent commit contributed a [https://phabricator.haskell.org/diffusion/GHC/browse/master/compiler/types/Type.hs;a483e711da7834bc952367f554ac4e877b4e157a$1191 Note] that explains why we need the dreaded KPush rule to be implemented in `splitTyConApp`. Without KPush there, it's possible that we can have two types t1 and t2 such that {{{t1 `eqType` t2}}} and yet they respond differently to `splitTyConApp`: t1 = `(T > co1) (a > co2)` and t2 = `T a`. Both t1 and t2 are wellkinded and can have the same kind. But one is a `TyConApp` and one is an `AppTy`. (Actually, looking at this, perhaps the magic will be in `mkAppTy`, not `splitTyConApp`.) But I have to look closer.\r\n\r\nThis ticket serves as a reminder to do so.","type_of_failure":"OtherFailure","blocking":[]} >A recent commit contributed a [Note](https://phabricator.haskell.org/diffusion/GHC/browse/master/compiler/types/Type.hs;a483e711da7834bc952367f554ac4e877b4e157a$1191) that explains why we need the dreaded KPush rule to be implemented in `splitTyConApp`. Without KPush there, it's possible that we can have two types t1 and t2 such that `t1 `eqType` t2` and yet they respond differently to `splitTyConApp`: t1 = `(T > co1) (a > co2)` and t2 = `T a`. Both t1 and t2 are wellkinded and can have the same kind. But one is a `TyConApp` and one is an `AppTy`. (Actually, looking at this, perhaps the magic will be in `mkAppTy`, not `splitTyConApp`.) But I have to look closer.
This ticket serves as a reminder to do so.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  
 Type  Task 
 TypeOfFailure  OtherFailure 
 Priority  high 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Implement KPush in types","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"A recent commit contributed a [https://phabricator.haskell.org/diffusion/GHC/browse/master/compiler/types/Type.hs;a483e711da7834bc952367f554ac4e877b4e157a$1191 Note] that explains why we need the dreaded KPush rule to be implemented in `splitTyConApp`. Without KPush there, it's possible that we can have two types t1 and t2 such that {{{t1 `eqType` t2}}} and yet they respond differently to `splitTyConApp`: t1 = `(T > co1) (a > co2)` and t2 = `T a`. Both t1 and t2 are wellkinded and can have the same kind. But one is a `TyConApp` and one is an `AppTy`. (Actually, looking at this, perhaps the magic will be in `mkAppTy`, not `splitTyConApp`.) But I have to look closer.\r\n\r\nThis ticket serves as a reminder to do so.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/issues/13643Core lint error with TypeInType and TypeFamilyDependencies20190707T18:20:49ZIcelandjackCore lint error with TypeInType and TypeFamilyDependenciesIn the code
```hs
{# Language TypeFamilyDependencies #}
{# Language RankNTypes #}
{# Language KindSignatures #}
{# Language DataKinds #}
{# Language TypeInType #}
{# Language GADTs #}
import Data.Kind (Type)
data Code = I
type family
Interp (a :: Code) = (res :: Type)  res > a where
Interp I = Bool
data T :: forall a. Interp a > Type where
MkNat :: T False
instance Show (T a) where show _ = "MkNat"
main = do
print MkNat
```
but add `{# Options_GHC dcorelint #}` and we get the attached log from running `runghc /tmp/tPb2.hs > /tmp/tPb2.log`.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  #12102 
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Core lint error with TypeInType and TypeFamilyDependencies","status":"New","operating_system":"","component":"Compiler","related":[12102],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["InjectiveFamilies,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"In the code\r\n\r\n{{{#!hs\r\n{# Language TypeFamilyDependencies #}\r\n{# Language RankNTypes #}\r\n{# Language KindSignatures #}\r\n{# Language DataKinds #}\r\n{# Language TypeInType #}\r\n{# Language GADTs #}\r\n\r\nimport Data.Kind (Type)\r\n\r\ndata Code = I\r\n\r\ntype family\r\n Interp (a :: Code) = (res :: Type)  res > a where\r\n Interp I = Bool\r\n\r\ndata T :: forall a. Interp a > Type where\r\n MkNat :: T False\r\n\r\ninstance Show (T a) where show _ = \"MkNat\"\r\n\r\nmain = do\r\n print MkNat\r\n}}}\r\n\r\nbut add `{# Options_GHC dcorelint #}` and we get the attached log from running `runghc /tmp/tPb2.hs > /tmp/tPb2.log`.\r\n","type_of_failure":"OtherFailure","blocking":[]} >In the code
```hs
{# Language TypeFamilyDependencies #}
{# Language RankNTypes #}
{# Language KindSignatures #}
{# Language DataKinds #}
{# Language TypeInType #}
{# Language GADTs #}
import Data.Kind (Type)
data Code = I
type family
Interp (a :: Code) = (res :: Type)  res > a where
Interp I = Bool
data T :: forall a. Interp a > Type where
MkNat :: T False
instance Show (T a) where show _ = "MkNat"
main = do
print MkNat
```
but add `{# Options_GHC dcorelint #}` and we get the attached log from running `runghc /tmp/tPb2.hs > /tmp/tPb2.log`.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  #12102 
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Core lint error with TypeInType and TypeFamilyDependencies","status":"New","operating_system":"","component":"Compiler","related":[12102],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["InjectiveFamilies,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"In the code\r\n\r\n{{{#!hs\r\n{# Language TypeFamilyDependencies #}\r\n{# Language RankNTypes #}\r\n{# Language KindSignatures #}\r\n{# Language DataKinds #}\r\n{# Language TypeInType #}\r\n{# Language GADTs #}\r\n\r\nimport Data.Kind (Type)\r\n\r\ndata Code = I\r\n\r\ntype family\r\n Interp (a :: Code) = (res :: Type)  res > a where\r\n Interp I = Bool\r\n\r\ndata T :: forall a. Interp a > Type where\r\n MkNat :: T False\r\n\r\ninstance Show (T a) where show _ = \"MkNat\"\r\n\r\nmain = do\r\n print MkNat\r\n}}}\r\n\r\nbut add `{# Options_GHC dcorelint #}` and we get the attached log from running `runghc /tmp/tPb2.hs > /tmp/tPb2.log`.\r\n","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc/issues/13625GHC internal error: ‘Y’ is not in scope during type checking, but it passed t...20190707T18:20:53ZMatthew PickeringGHC internal error: ‘Y’ is not in scope during type checking, but it passed the renamer```
{# LANGUAGE TypeInType #}
data X :: Y where Y :: X
```
The error message is:
```
Bug.hs:2:11: error: …
• GHC internal error: ‘Y’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: [r1cR :> APromotionErr TyConPE]
• In the kind ‘Y’
```
Originally reported by \@mietek in #11821
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  mietek 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC internal error: ‘Y’ is not in scope during type checking, but it passed the renamer","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["mietek"],"type":"Bug","description":"{{{\r\n{# LANGUAGE TypeInType #}\r\ndata X :: Y where Y :: X\r\n}}}\r\n\r\nThe error message is:\r\n\r\n{{{\r\nBug.hs:2:11: error: …\r\n • GHC internal error: ‘Y’ is not in scope during type checking, but it passed the renamer\r\n tcl_env of environment: [r1cR :> APromotionErr TyConPE]\r\n • In the kind ‘Y’\r\n}}}\r\n\r\nOriginally reported by @mietek in #11821","type_of_failure":"OtherFailure","blocking":[]} >```
{# LANGUAGE TypeInType #}
data X :: Y where Y :: X
```
The error message is:
```
Bug.hs:2:11: error: …
• GHC internal error: ‘Y’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: [r1cR :> APromotionErr TyConPE]
• In the kind ‘Y’
```
Originally reported by \@mietek in #11821
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  mietek 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC internal error: ‘Y’ is not in scope during type checking, but it passed the renamer","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["mietek"],"type":"Bug","description":"{{{\r\n{# LANGUAGE TypeInType #}\r\ndata X :: Y where Y :: X\r\n}}}\r\n\r\nThe error message is:\r\n\r\n{{{\r\nBug.hs:2:11: error: …\r\n • GHC internal error: ‘Y’ is not in scope during type checking, but it passed the renamer\r\n tcl_env of environment: [r1cR :> APromotionErr TyConPE]\r\n • In the kind ‘Y’\r\n}}}\r\n\r\nOriginally reported by @mietek in #11821","type_of_failure":"OtherFailure","blocking":[]} >8.2.1https://gitlab.haskell.org/ghc/ghc/issues/13603Can't resolve levity polymorphic superclass20190707T18:21:04ZIcelandjackCan't resolve levity polymorphic superclassThis works
```hs
{# Language PolyKinds, TypeInType #}
import GHC.Exts (TYPE, RuntimeRep)
class A (a :: TYPE rep)
class A a => B (a :: TYPE rep)
instance A b => A (a > (b :: TYPE rep))
instance B b => B (a > b)
```
but the moment you add (`b :: TYPE rep`) to the last line it stops working
```hs
 t3I7.hs:9:1040: error: …
 • Could not deduce (A b)
 arising from the superclasses of an instance declaration
 from the context: B b
 bound by the instance declaration at /tmp/t3I7.hs:9:1040
 • In the instance declaration for ‘B (a > b)’
 Compilation failed.
{# Language PolyKinds, TypeInType #}
import GHC.Exts (TYPE, RuntimeRep)
class A (a :: TYPE rep)
class A a => B (a :: TYPE rep)
instance A b => A (a > (b :: TYPE rep))
instance B b => B (a > (b :: TYPE rep))
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 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":"Can't resolve levity polymorphic superclass","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["LevityPolymorphism,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This works\r\n\r\n{{{#!hs\r\n{# Language PolyKinds, TypeInType #}\r\n\r\nimport GHC.Exts (TYPE, RuntimeRep)\r\n\r\nclass A (a :: TYPE rep)\r\nclass A a => B (a :: TYPE rep)\r\n\r\ninstance A b => A (a > (b :: TYPE rep))\r\ninstance B b => B (a > b)\r\n}}}\r\n\r\nbut the moment you add (`b :: TYPE rep`) to the last line it stops working\r\n\r\n\r\n{{{#!hs\r\n t3I7.hs:9:1040: error: …\r\n • Could not deduce (A b)\r\n arising from the superclasses of an instance declaration\r\n from the context: B b\r\n bound by the instance declaration at /tmp/t3I7.hs:9:1040\r\n • In the instance declaration for ‘B (a > b)’\r\n Compilation failed.\r\n\r\n{# Language PolyKinds, TypeInType #}\r\n\r\nimport GHC.Exts (TYPE, RuntimeRep)\r\n\r\nclass A (a :: TYPE rep)\r\nclass A a => B (a :: TYPE rep)\r\n\r\ninstance A b => A (a > (b :: TYPE rep))\r\ninstance B b => B (a > (b :: TYPE rep))\r\n}}}\r\n\r\n\r\n","type_of_failure":"OtherFailure","blocking":[]} >This works
```hs
{# Language PolyKinds, TypeInType #}
import GHC.Exts (TYPE, RuntimeRep)
class A (a :: TYPE rep)
class A a => B (a :: TYPE rep)
instance A b => A (a > (b :: TYPE rep))
instance B b => B (a > b)
```
but the moment you add (`b :: TYPE rep`) to the last line it stops working
```hs
 t3I7.hs:9:1040: error: …
 • Could not deduce (A b)
 arising from the superclasses of an instance declaration
 from the context: B b
 bound by the instance declaration at /tmp/t3I7.hs:9:1040
 • In the instance declaration for ‘B (a > b)’
 Compilation failed.
{# Language PolyKinds, TypeInType #}
import GHC.Exts (TYPE, RuntimeRep)
class A (a :: TYPE rep)
class A a => B (a :: TYPE rep)
instance A b => A (a > (b :: TYPE rep))
instance B b => B (a > (b :: TYPE rep))
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 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":"Can't resolve levity polymorphic superclass","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["LevityPolymorphism,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This works\r\n\r\n{{{#!hs\r\n{# Language PolyKinds, TypeInType #}\r\n\r\nimport GHC.Exts (TYPE, RuntimeRep)\r\n\r\nclass A (a :: TYPE rep)\r\nclass A a => B (a :: TYPE rep)\r\n\r\ninstance A b => A (a > (b :: TYPE rep))\r\ninstance B b => B (a > b)\r\n}}}\r\n\r\nbut the moment you add (`b :: TYPE rep`) to the last line it stops working\r\n\r\n\r\n{{{#!hs\r\n t3I7.hs:9:1040: error: …\r\n • Could not deduce (A b)\r\n arising from the superclasses of an instance declaration\r\n from the context: B b\r\n bound by the instance declaration at /tmp/t3I7.hs:9:1040\r\n • In the instance declaration for ‘B (a > b)’\r\n Compilation failed.\r\n\r\n{# Language PolyKinds, TypeInType #}\r\n\r\nimport GHC.Exts (TYPE, RuntimeRep)\r\n\r\nclass A (a :: TYPE rep)\r\nclass A a => B (a :: TYPE rep)\r\n\r\ninstance A b => A (a > (b :: TYPE rep))\r\ninstance B b => B (a > (b :: TYPE rep))\r\n}}}\r\n\r\n\r\n","type_of_failure":"OtherFailure","blocking":[]} >8.2.1https://gitlab.haskell.org/ghc/ghc/issues/13585ala from Control.Lens.Wrapped panics20190707T18:21:10ZFumiaki Kinoshitaala from Control.Lens.Wrapped panicsPanic.hs:
```
module Panic where
import Control.Lens.Wrapped
import Data.Monoid
foo :: Maybe String
foo = ala Last foldMap [Just "foo"]
```
main.hs:
```
module Main where
import Panic (foo)
main :: IO ()
main = print foo
```
```
$ ghc c O2 Panic.hs
$ ghc c O2 main.hs
ghc: panic! (the 'impossible' happened)
(GHC version 8.2.0.20170404 for x86_64unknownlinux):
splitTyConApp
(Exchange (Unwrapped (Last String)) (Unwrapped (Last String)) > <*
> * > *>_N) (Maybe
[Char]) ((Identity > <*
> *>_N) (Maybe
[Char]))
Call stack:
CallStack (from HasCallStack):
prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1134:58 in ghc:Outputable
callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:1105:34 in ghc:Type
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
The GHC version is 8134f7d4ba2c14b2f24d2f4c1f5260fcaff3304a.
Control.Lens.Wrapped is from the latest version of lens on GitHub: https://github.com/ekmett/lens/blob/9c4447de7ef57f67dbe293320d45bd8a546be522/src/Control/Lens/Wrapped.hsPanic.hs:
```
module Panic where
import Control.Lens.Wrapped
import Data.Monoid
foo :: Maybe String
foo = ala Last foldMap [Just "foo"]
```
main.hs:
```
module Main where
import Panic (foo)
main :: IO ()
main = print foo
```
```
$ ghc c O2 Panic.hs
$ ghc c O2 main.hs
ghc: panic! (the 'impossible' happened)
(GHC version 8.2.0.20170404 for x86_64unknownlinux):
splitTyConApp
(Exchange (Unwrapped (Last String)) (Unwrapped (Last String)) > <*
> * > *>_N) (Maybe
[Char]) ((Identity > <*
> *>_N) (Maybe
[Char]))
Call stack:
CallStack (from HasCallStack):
prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1134:58 in ghc:Outputable
callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:1105:34 in ghc:Type
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
The GHC version is 8134f7d4ba2c14b2f24d2f4c1f5260fcaff3304a.
Control.Lens.Wrapped is from the latest version of lens on GitHub: https://github.com/ekmett/lens/blob/9c4447de7ef57f67dbe293320d45bd8a546be522/src/Control/Lens/Wrapped.hs8.2.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/issues/13555Typechecker regression when combining PolyKinds and MonoLocalBinds20190707T18:21:21ZRyan ScottTypechecker regression when combining PolyKinds and MonoLocalBinds`lol0.6.0.0` from Hackage currently fails to build with GHC 8.2.1 because of this regression. Here is a minimized example:
```hs
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE InstanceSigs #}
{# LANGUAGE MonoLocalBinds #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
module Crypto.Lol.Types.FiniteField (GF(..)) where
import Data.Functor.Identity (Identity(..))
data T a
type Polynomial a = T a
newtype GF fp d = GF (Polynomial fp)
type CRTInfo r = (Int > r, r)
type Tagged s b = TaggedT s Identity b
newtype TaggedT s m b = TagT { untagT :: m b }
class Reflects a i where
value :: Tagged a i
class CRTrans mon r where
crtInfo :: Reflects m Int => TaggedT m mon (CRTInfo r)
instance CRTrans Maybe (GF fp d) where
crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))
crtInfo = undefined
```
This typechecks OK with GHC 8.0.2, but with 8.2.1, it complains:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.0.20170403: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Crypto.Lol.Types.FiniteField ( Bug.hs, interpreted )
Bug.hs:25:14: error:
• Couldn't match type ‘k0’ with ‘k2’
because type variable ‘k2’ would escape its scope
This (rigid, skolem) type variable is bound by
the type signature for:
crtInfo :: forall k2 (m :: k2).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
at Bug.hs:25:1479
Expected type: TaggedT m Maybe (CRTInfo (GF fp d))
Actual type: TaggedT m Maybe (CRTInfo (GF fp d))
• When checking that instance signature for ‘crtInfo’
is more general than its signature in the class
Instance sig: forall (m :: k0).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
Class sig: forall k2 (m :: k2).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
In the instance declaration for ‘CRTrans Maybe (GF fp d)’

25  crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Bug.hs:25:14: error:
• Could not deduce (Reflects m Int)
from the context: Reflects m Int
bound by the type signature for:
crtInfo :: forall k2 (m :: k2).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
at Bug.hs:25:1479
The type variable ‘k0’ is ambiguous
• When checking that instance signature for ‘crtInfo’
is more general than its signature in the class
Instance sig: forall (m :: k0).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
Class sig: forall k2 (m :: k2).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
In the instance declaration for ‘CRTrans Maybe (GF fp d)’

25  crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Notably, both `PolyKinds` and `MonoLocalBinds` are required to trigger this bug.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  highest 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Typechecker regression when combining PolyKinds and MonoLocalBinds","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"`lol0.6.0.0` from Hackage currently fails to build with GHC 8.2.1 because of this regression. Here is a minimized example:\r\n\r\n{{{#!hs\r\n{# LANGUAGE FlexibleContexts #}\r\n{# LANGUAGE InstanceSigs #}\r\n{# LANGUAGE MonoLocalBinds #}\r\n{# LANGUAGE MultiParamTypeClasses #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE RankNTypes #}\r\nmodule Crypto.Lol.Types.FiniteField (GF(..)) where\r\n\r\nimport Data.Functor.Identity (Identity(..))\r\n\r\ndata T a\r\ntype Polynomial a = T a\r\nnewtype GF fp d = GF (Polynomial fp)\r\ntype CRTInfo r = (Int > r, r)\r\ntype Tagged s b = TaggedT s Identity b\r\nnewtype TaggedT s m b = TagT { untagT :: m b }\r\n\r\nclass Reflects a i where\r\n value :: Tagged a i\r\n\r\nclass CRTrans mon r where\r\n crtInfo :: Reflects m Int => TaggedT m mon (CRTInfo r)\r\n\r\ninstance CRTrans Maybe (GF fp d) where\r\n crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))\r\n crtInfo = undefined\r\n}}}\r\n\r\nThis typechecks OK with GHC 8.0.2, but with 8.2.1, it complains:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.0.20170403: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Crypto.Lol.Types.FiniteField ( Bug.hs, interpreted )\r\n\r\nBug.hs:25:14: error:\r\n • Couldn't match type ‘k0’ with ‘k2’\r\n because type variable ‘k2’ would escape its scope\r\n This (rigid, skolem) type variable is bound by\r\n the type signature for:\r\n crtInfo :: forall k2 (m :: k2).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n at Bug.hs:25:1479\r\n Expected type: TaggedT m Maybe (CRTInfo (GF fp d))\r\n Actual type: TaggedT m Maybe (CRTInfo (GF fp d))\r\n • When checking that instance signature for ‘crtInfo’\r\n is more general than its signature in the class\r\n Instance sig: forall (m :: k0).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n Class sig: forall k2 (m :: k2).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n In the instance declaration for ‘CRTrans Maybe (GF fp d)’\r\n \r\n25  crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n\r\nBug.hs:25:14: error:\r\n • Could not deduce (Reflects m Int)\r\n from the context: Reflects m Int\r\n bound by the type signature for:\r\n crtInfo :: forall k2 (m :: k2).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n at Bug.hs:25:1479\r\n The type variable ‘k0’ is ambiguous\r\n • When checking that instance signature for ‘crtInfo’\r\n is more general than its signature in the class\r\n Instance sig: forall (m :: k0).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n Class sig: forall k2 (m :: k2).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n In the instance declaration for ‘CRTrans Maybe (GF fp d)’\r\n \r\n25  crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nNotably, both `PolyKinds` and `MonoLocalBinds` are required to trigger this bug.","type_of_failure":"OtherFailure","blocking":[]} >`lol0.6.0.0` from Hackage currently fails to build with GHC 8.2.1 because of this regression. Here is a minimized example:
```hs
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE InstanceSigs #}
{# LANGUAGE MonoLocalBinds #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
module Crypto.Lol.Types.FiniteField (GF(..)) where
import Data.Functor.Identity (Identity(..))
data T a
type Polynomial a = T a
newtype GF fp d = GF (Polynomial fp)
type CRTInfo r = (Int > r, r)
type Tagged s b = TaggedT s Identity b
newtype TaggedT s m b = TagT { untagT :: m b }
class Reflects a i where
value :: Tagged a i
class CRTrans mon r where
crtInfo :: Reflects m Int => TaggedT m mon (CRTInfo r)
instance CRTrans Maybe (GF fp d) where
crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))
crtInfo = undefined
```
This typechecks OK with GHC 8.0.2, but with 8.2.1, it complains:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.0.20170403: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Crypto.Lol.Types.FiniteField ( Bug.hs, interpreted )
Bug.hs:25:14: error:
• Couldn't match type ‘k0’ with ‘k2’
because type variable ‘k2’ would escape its scope
This (rigid, skolem) type variable is bound by
the type signature for:
crtInfo :: forall k2 (m :: k2).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
at Bug.hs:25:1479
Expected type: TaggedT m Maybe (CRTInfo (GF fp d))
Actual type: TaggedT m Maybe (CRTInfo (GF fp d))
• When checking that instance signature for ‘crtInfo’
is more general than its signature in the class
Instance sig: forall (m :: k0).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
Class sig: forall k2 (m :: k2).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
In the instance declaration for ‘CRTrans Maybe (GF fp d)’

25  crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Bug.hs:25:14: error:
• Could not deduce (Reflects m Int)
from the context: Reflects m Int
bound by the type signature for:
crtInfo :: forall k2 (m :: k2).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
at Bug.hs:25:1479
The type variable ‘k0’ is ambiguous
• When checking that instance signature for ‘crtInfo’
is more general than its signature in the class
Instance sig: forall (m :: k0).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
Class sig: forall k2 (m :: k2).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
In the instance declaration for ‘CRTrans Maybe (GF fp d)’

25  crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Notably, both `PolyKinds` and `MonoLocalBinds` are required to trigger this bug.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  highest 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Typechecker regression when combining PolyKinds and MonoLocalBinds","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"`lol0.6.0.0` from Hackage currently fails to build with GHC 8.2.1 because of this regression. Here is a minimized example:\r\n\r\n{{{#!hs\r\n{# LANGUAGE FlexibleContexts #}\r\n{# LANGUAGE InstanceSigs #}\r\n{# LANGUAGE MonoLocalBinds #}\r\n{# LANGUAGE MultiParamTypeClasses #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE RankNTypes #}\r\nmodule Crypto.Lol.Types.FiniteField (GF(..)) where\r\n\r\nimport Data.Functor.Identity (Identity(..))\r\n\r\ndata T a\r\ntype Polynomial a = T a\r\nnewtype GF fp d = GF (Polynomial fp)\r\ntype CRTInfo r = (Int > r, r)\r\ntype Tagged s b = TaggedT s Identity b\r\nnewtype TaggedT s m b = TagT { untagT :: m b }\r\n\r\nclass Reflects a i where\r\n value :: Tagged a i\r\n\r\nclass CRTrans mon r where\r\n crtInfo :: Reflects m Int => TaggedT m mon (CRTInfo r)\r\n\r\ninstance CRTrans Maybe (GF fp d) where\r\n crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))\r\n crtInfo = undefined\r\n}}}\r\n\r\nThis typechecks OK with GHC 8.0.2, but with 8.2.1, it complains:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.0.20170403: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Crypto.Lol.Types.FiniteField ( Bug.hs, interpreted )\r\n\r\nBug.hs:25:14: error:\r\n • Couldn't match type ‘k0’ with ‘k2’\r\n because type variable ‘k2’ would escape its scope\r\n This (rigid, skolem) type variable is bound by\r\n the type signature for:\r\n crtInfo :: forall k2 (m :: k2).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n at Bug.hs:25:1479\r\n Expected type: TaggedT m Maybe (CRTInfo (GF fp d))\r\n Actual type: TaggedT m Maybe (CRTInfo (GF fp d))\r\n • When checking that instance signature for ‘crtInfo’\r\n is more general than its signature in the class\r\n Instance sig: forall (m :: k0).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n Class sig: forall k2 (m :: k2).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n In the instance declaration for ‘CRTrans Maybe (GF fp d)’\r\n \r\n25  crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n\r\nBug.hs:25:14: error:\r\n • Could not deduce (Reflects m Int)\r\n from the context: Reflects m Int\r\n bound by the type signature for:\r\n crtInfo :: forall k2 (m :: k2).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n at Bug.hs:25:1479\r\n The type variable ‘k0’ is ambiguous\r\n • When checking that instance signature for ‘crtInfo’\r\n is more general than its signature in the class\r\n Instance sig: forall (m :: k0).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n Class sig: forall k2 (m :: k2).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n In the instance declaration for ‘CRTrans Maybe (GF fp d)’\r\n \r\n25  crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nNotably, both `PolyKinds` and `MonoLocalBinds` are required to trigger this bug.","type_of_failure":"OtherFailure","blocking":[]} >8.2.1https://gitlab.haskell.org/ghc/ghc/issues/13549GHC 8.2.1's typechecker rejects code generated by singletons that 8.0 accepts20190707T18:21:23ZRyan ScottGHC 8.2.1's typechecker rejects code generated by singletons that 8.0 acceptsI recently attempted to upgrade `singletons` to use GHC 8.2.1, but was thwarted when GHC's typechecker rejected code that was generated by Template Haskell. I was able to put all of this code in a single module (which I've attached), but sadly, it's 1367 lines long. What's important is that GHC 8.0.1 and 8.0.2 accept this code, but neither 8.2.1rc1 nor HEAD do. Here is the error message you get, in its full glory:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs fprintexplicitkinds
GHCi, version 8.2.0.20170403: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:1328:59: error:
• Couldn't match type ‘c69895866216793215480’ with ‘[a_a337f]’
‘c69895866216793215480’ is untouchable
inside the constraints: (arg_a33hh ~ xs_a33fp, arg_a33hi ~ r_a33fq)
bound by the type signature for:
lambda_a33iH :: forall (xs_a33fp :: [a_a337f]) (r_a33fq :: [[a_a337f]]).
(arg_a33hh ~ xs_a33fp, arg_a33hi ~ r_a33fq) =>
Sing [a_a337f] xs_a33fp
> Sing [[a_a337f]] r_a33fq
> Sing
[[a_a337f]]
(Apply
[[a_a337f]]
[[a_a337f]]
(Apply
[a_a337f]
(TyFun [[a_a337f]] [[a_a337f]] > *)
(Let6989586621679736980InterleaveSym4
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33hh)
arg_a33hi)
at Bug.hs:(1289,35)(1294,157)
Expected type: Sing (TyFun [a_a337f] [a_a337f] > *) t
> Sing [a_a337f] t1
> Sing [[a_a337f]] t2
> Sing
([a_a337f], [[a_a337f]])
((@@)
[[a_a337f]]
([a_a337f], [[a_a337f]])
((@@)
[a_a337f]
([[a_a337f]] ~> ([a_a337f], [[a_a337f]]))
((@@)
(TyFun [a_a337f] [a_a337f] > *)
([a_a337f] ~> ([[a_a337f]] ~> ([a_a337f], [[a_a337f]])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
[a_a337f]
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
t)
t1)
t2)
Actual type: Sing (TyFun [a_a337f] c69895866216793215480 > *) t
> Sing [a_a337f] t1
> Sing [c69895866216793215480] t2
> Sing
([a_a337f], [c69895866216793215480])
(Apply
[c69895866216793215480]
([a_a337f], [c69895866216793215480])
(Apply
[a_a337f]
([c69895866216793215480] ~> ([a_a337f], [c69895866216793215480]))
(Apply
(TyFun [a_a337f] c69895866216793215480 > *)
([a_a337f]
~> ([c69895866216793215480]
~> ([a_a337f], [c69895866216793215480])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
c69895866216793215480
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
t)
t1)
t2)
• In the second argument of ‘singFun3’, namely ‘sInterleave'’
In the first argument of ‘applySing’, namely
‘((singFun3
(Proxy ::
Proxy (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO)))
sInterleave')’
In the first argument of ‘applySing’, namely
‘((applySing
((singFun3
(Proxy ::
Proxy (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO)))
sInterleave'))
((singFun1 (Proxy :: Proxy IdSym0)) sId))’
• Relevant bindings include
sX_6989586621679737266 :: Sing
([a_a337f], [[a_a337f]])
(Let6989586621679737265X_6989586621679737266Sym6
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO
xs_a33fp
r_a33fq)
(bound at Bug.hs:1321:41)
r_a33iK :: Sing [[a_a337f]] r_a33fq (bound at Bug.hs:1295:57)
xs_a33iJ :: Sing [a_a337f] xs_a33fp (bound at Bug.hs:1295:48)
lambda_a33iH :: Sing [a_a337f] xs_a33fp
> Sing [[a_a337f]] r_a33fq
> Sing
[[a_a337f]]
(Apply
[[a_a337f]]
[[a_a337f]]
(Apply
[a_a337f]
(TyFun [[a_a337f]] [[a_a337f]] > *)
(Let6989586621679736980InterleaveSym4
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33hh)
arg_a33hi)
(bound at Bug.hs:1295:35)
sR :: Sing [[a_a337f]] arg_a33hi (bound at Bug.hs:1287:45)
sXs :: Sing [a_a337f] arg_a33hh (bound at Bug.hs:1287:41)
sInterleave' :: forall (arg_a33he :: TyFun
[a_a337f] c69895866216793215480
> *) (arg_a33hf :: [a_a337f]) (arg_a33hg :: [c69895866216793215480]).
Sing (TyFun [a_a337f] c69895866216793215480 > *) arg_a33he
> Sing [a_a337f] arg_a33hf
> Sing [c69895866216793215480] arg_a33hg
> Sing
([a_a337f], [c69895866216793215480])
(Apply
[c69895866216793215480]
([a_a337f], [c69895866216793215480])
(Apply
[a_a337f]
([c69895866216793215480] ~> ([a_a337f], [c69895866216793215480]))
(Apply
(TyFun [a_a337f] c69895866216793215480 > *)
([a_a337f]
~> ([c69895866216793215480]
~> ([a_a337f], [c69895866216793215480])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
c69895866216793215480
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33he)
arg_a33hf)
arg_a33hg)
(bound at Bug.hs:1166:29)
lambda_a33ha :: Sing a_a337f t_a33aL
> Sing [a_a337f] ts_a33aM
> Sing [a_a337f] is_a33aO
> Sing
[[a_a337f]]
(Apply
[a_a337f]
[[a_a337f]]
(Apply
[a_a337f]
([a_a337f] ~> [[a_a337f]])
(Let6989586621679736931PermsSym1 a_a337f xs0_a33a0)
arg_a33h0)
arg_a33h1)
(bound at Bug.hs:1153:23)
sTs :: Sing [a_a337f] n_a1kQd (bound at Bug.hs:1143:34)
sT :: Sing a_a337f n_a1kQc (bound at Bug.hs:1143:31)
lambda_a33gY :: Sing [a_a337f] xs0_a33a0
> Sing
[[a_a337f]]
(Apply [a_a337f] [[a_a337f]] (PermutationsSym0 a_a337f) t_a33gX)
(bound at Bug.hs:1127:11)
(Some bindings suppressed; use fmaxrelevantbinds=N or fnomaxrelevantbinds)

1328  sInterleave'))
 ^^^^^^^^^^^^
Bug.hs:1328:59: error:
• Could not deduce: (Let6989586621679736980Interleave'
[a_a337f]
[a_a337f]
a_a337f
c69895866216793215480
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO
t
t1
t2 :: ([a_a337f], [c69895866216793215480]))
~~
(Let6989586621679736980Interleave'
[a_a337f]
[a_a337f]
a_a337f
[a_a337f]
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO
t
t1
t2 :: ([a_a337f], [c69895866216793215480]))
from the context: t_a33gX ~ xs0_a33a0
bound by the type signature for:
lambda_a33gY :: forall (xs0_a33a0 :: [a_a337f]).
t_a33gX ~ xs0_a33a0 =>
Sing [a_a337f] xs0_a33a0
> Sing
[[a_a337f]]
(Apply
[a_a337f] [[a_a337f]] (PermutationsSym0 a_a337f) t_a33gX)
at Bug.hs:(1122,11)(1126,67)
or from: arg_a33h0 ~ (':) a_a337f n_a1kQc n_a1kQd
bound by a pattern with constructor:
SCons :: forall a_11 (z_a1kQb :: [a_11]) (n_a1kQc :: a_11) (n_a1kQd :: [a_11]).
z_a1kQb ~ (':) a_11 n_a1kQc n_a1kQd =>
Sing a_11 n_a1kQc > Sing [a_11] n_a1kQd > Sing [a_11] z_a1kQb,
in an equation for ‘sPerms’
at Bug.hs:1143:2536
or from: (arg_a33h0
~
Apply
[a_a337f]
[a_a337f]
(Apply
a_a337f (TyFun [a_a337f] [a_a337f] > *) ((:$) a_a337f) t_a33aL)
ts_a33aM,
arg_a33h1 ~ is_a33aO)
bound by the type signature for:
lambda_a33ha :: forall (t_a33aL :: a_a337f) (ts_a33aM :: [a_a337f]) (is_a33aO :: [a_a337f]).
(arg_a33h0
~
Apply
[a_a337f]
[a_a337f]
(Apply
a_a337f
(TyFun [a_a337f] [a_a337f] > *)
((:$) a_a337f)
t_a33aL)
ts_a33aM,
arg_a33h1 ~ is_a33aO) =>
Sing a_a337f t_a33aL
> Sing [a_a337f] ts_a33aM
> Sing [a_a337f] is_a33aO
> Sing
[[a_a337f]]
(Apply
[a_a337f]
[[a_a337f]]
(Apply
[a_a337f]
([a_a337f] ~> [[a_a337f]])
(Let6989586621679736931PermsSym1 a_a337f xs0_a33a0)
arg_a33h0)
arg_a33h1)
at Bug.hs:(1145,23)(1152,117)
or from: (arg_a33hh ~ xs_a33fp, arg_a33hi ~ r_a33fq)
bound by the type signature for:
lambda_a33iH :: forall (xs_a33fp :: [a_a337f]) (r_a33fq :: [[a_a337f]]).
(arg_a33hh ~ xs_a33fp, arg_a33hi ~ r_a33fq) =>
Sing [a_a337f] xs_a33fp
> Sing [[a_a337f]] r_a33fq
> Sing
[[a_a337f]]
(Apply
[[a_a337f]]
[[a_a337f]]
(Apply
[a_a337f]
(TyFun [[a_a337f]] [[a_a337f]] > *)
(Let6989586621679736980InterleaveSym4
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33hh)
arg_a33hi)
at Bug.hs:(1289,35)(1294,157)
Expected type: Sing (TyFun [a_a337f] [a_a337f] > *) t
> Sing [a_a337f] t1
> Sing [[a_a337f]] t2
> Sing
([a_a337f], [[a_a337f]])
((@@)
[[a_a337f]]
([a_a337f], [[a_a337f]])
((@@)
[a_a337f]
([[a_a337f]] ~> ([a_a337f], [[a_a337f]]))
((@@)
(TyFun [a_a337f] [a_a337f] > *)
([a_a337f] ~> ([[a_a337f]] ~> ([a_a337f], [[a_a337f]])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
[a_a337f]
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
t)
t1)
t2)
Actual type: Sing (TyFun [a_a337f] c69895866216793215480 > *) t
> Sing [a_a337f] t1
> Sing [c69895866216793215480] t2
> Sing
([a_a337f], [c69895866216793215480])
(Apply
[c69895866216793215480]
([a_a337f], [c69895866216793215480])
(Apply
[a_a337f]
([c69895866216793215480] ~> ([a_a337f], [c69895866216793215480]))
(Apply
(TyFun [a_a337f] c69895866216793215480 > *)
([a_a337f]
~> ([c69895866216793215480]
~> ([a_a337f], [c69895866216793215480])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
c69895866216793215480
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
t)
t1)
t2)
The type variable ‘c69895866216793215480’ is ambiguous
• In the second argument of ‘singFun3’, namely ‘sInterleave'’
In the first argument of ‘applySing’, namely
‘((singFun3
(Proxy ::
Proxy (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO)))
sInterleave')’
In the first argument of ‘applySing’, namely
‘((applySing
((singFun3
(Proxy ::
Proxy (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO)))
sInterleave'))
((singFun1 (Proxy :: Proxy IdSym0)) sId))’
• Relevant bindings include
sX_6989586621679737266 :: Sing
([a_a337f], [[a_a337f]])
(Let6989586621679737265X_6989586621679737266Sym6
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO
xs_a33fp
r_a33fq)
(bound at Bug.hs:1321:41)
r_a33iK :: Sing [[a_a337f]] r_a33fq (bound at Bug.hs:1295:57)
xs_a33iJ :: Sing [a_a337f] xs_a33fp (bound at Bug.hs:1295:48)
lambda_a33iH :: Sing [a_a337f] xs_a33fp
> Sing [[a_a337f]] r_a33fq
> Sing
[[a_a337f]]
(Apply
[[a_a337f]]
[[a_a337f]]
(Apply
[a_a337f]
(TyFun [[a_a337f]] [[a_a337f]] > *)
(Let6989586621679736980InterleaveSym4
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33hh)
arg_a33hi)
(bound at Bug.hs:1295:35)
sR :: Sing [[a_a337f]] arg_a33hi (bound at Bug.hs:1287:45)
sXs :: Sing [a_a337f] arg_a33hh (bound at Bug.hs:1287:41)
sInterleave' :: forall (arg_a33he :: TyFun
[a_a337f] c69895866216793215480
> *) (arg_a33hf :: [a_a337f]) (arg_a33hg :: [c69895866216793215480]).
Sing (TyFun [a_a337f] c69895866216793215480 > *) arg_a33he
> Sing [a_a337f] arg_a33hf
> Sing [c69895866216793215480] arg_a33hg
> Sing
([a_a337f], [c69895866216793215480])
(Apply
[c69895866216793215480]
([a_a337f], [c69895866216793215480])
(Apply
[a_a337f]
([c69895866216793215480] ~> ([a_a337f], [c69895866216793215480]))
(Apply
(TyFun [a_a337f] c69895866216793215480 > *)
([a_a337f]
~> ([c69895866216793215480]
~> ([a_a337f], [c69895866216793215480])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
c69895866216793215480
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33he)
arg_a33hf)
arg_a33hg)
(bound at Bug.hs:1166:29)
lambda_a33ha :: Sing a_a337f t_a33aL
> Sing [a_a337f] ts_a33aM
> Sing [a_a337f] is_a33aO
> Sing
[[a_a337f]]
(Apply
[a_a337f]
[[a_a337f]]
(Apply
[a_a337f]
([a_a337f] ~> [[a_a337f]])
(Let6989586621679736931PermsSym1 a_a337f xs0_a33a0)
arg_a33h0)
arg_a33h1)
(bound at Bug.hs:1153:23)
sTs :: Sing [a_a337f] n_a1kQd (bound at Bug.hs:1143:34)
sT :: Sing a_a337f n_a1kQc (bound at Bug.hs:1143:31)
lambda_a33gY :: Sing [a_a337f] xs0_a33a0
> Sing
[[a_a337f]]
(Apply [a_a337f] [[a_a337f]] (PermutationsSym0 a_a337f) t_a33gX)
(bound at Bug.hs:1127:11)
(Some bindings suppressed; use fmaxrelevantbinds=N or fnomaxrelevantbinds)

1328  sInterleave'))
 ^^^^^^^^^^^^
```I recently attempted to upgrade `singletons` to use GHC 8.2.1, but was thwarted when GHC's typechecker rejected code that was generated by Template Haskell. I was able to put all of this code in a single module (which I've attached), but sadly, it's 1367 lines long. What's important is that GHC 8.0.1 and 8.0.2 accept this code, but neither 8.2.1rc1 nor HEAD do. Here is the error message you get, in its full glory:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs fprintexplicitkinds
GHCi, version 8.2.0.20170403: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:1328:59: error:
• Couldn't match type ‘c69895866216793215480’ with ‘[a_a337f]’
‘c69895866216793215480’ is untouchable
inside the constraints: (arg_a33hh ~ xs_a33fp, arg_a33hi ~ r_a33fq)
bound by the type signature for:
lambda_a33iH :: forall (xs_a33fp :: [a_a337f]) (r_a33fq :: [[a_a337f]]).
(arg_a33hh ~ xs_a33fp, arg_a33hi ~ r_a33fq) =>
Sing [a_a337f] xs_a33fp
> Sing [[a_a337f]] r_a33fq
> Sing
[[a_a337f]]
(Apply
[[a_a337f]]
[[a_a337f]]
(Apply
[a_a337f]
(TyFun [[a_a337f]] [[a_a337f]] > *)
(Let6989586621679736980InterleaveSym4
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33hh)
arg_a33hi)
at Bug.hs:(1289,35)(1294,157)
Expected type: Sing (TyFun [a_a337f] [a_a337f] > *) t
> Sing [a_a337f] t1
> Sing [[a_a337f]] t2
> Sing
([a_a337f], [[a_a337f]])
((@@)
[[a_a337f]]
([a_a337f], [[a_a337f]])
((@@)
[a_a337f]
([[a_a337f]] ~> ([a_a337f], [[a_a337f]]))
((@@)
(TyFun [a_a337f] [a_a337f] > *)
([a_a337f] ~> ([[a_a337f]] ~> ([a_a337f], [[a_a337f]])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
[a_a337f]
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
t)
t1)
t2)
Actual type: Sing (TyFun [a_a337f] c69895866216793215480 > *) t
> Sing [a_a337f] t1
> Sing [c69895866216793215480] t2
> Sing
([a_a337f], [c69895866216793215480])
(Apply
[c69895866216793215480]
([a_a337f], [c69895866216793215480])
(Apply
[a_a337f]
([c69895866216793215480] ~> ([a_a337f], [c69895866216793215480]))
(Apply
(TyFun [a_a337f] c69895866216793215480 > *)
([a_a337f]
~> ([c69895866216793215480]
~> ([a_a337f], [c69895866216793215480])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
c69895866216793215480
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
t)
t1)
t2)
• In the second argument of ‘singFun3’, namely ‘sInterleave'’
In the first argument of ‘applySing’, namely
‘((singFun3
(Proxy ::
Proxy (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO)))
sInterleave')’
In the first argument of ‘applySing’, namely
‘((applySing
((singFun3
(Proxy ::
Proxy (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO)))
sInterleave'))
((singFun1 (Proxy :: Proxy IdSym0)) sId))’
• Relevant bindings include
sX_6989586621679737266 :: Sing
([a_a337f], [[a_a337f]])
(Let6989586621679737265X_6989586621679737266Sym6
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO
xs_a33fp
r_a33fq)
(bound at Bug.hs:1321:41)
r_a33iK :: Sing [[a_a337f]] r_a33fq (bound at Bug.hs:1295:57)
xs_a33iJ :: Sing [a_a337f] xs_a33fp (bound at Bug.hs:1295:48)
lambda_a33iH :: Sing [a_a337f] xs_a33fp
> Sing [[a_a337f]] r_a33fq
> Sing
[[a_a337f]]
(Apply
[[a_a337f]]
[[a_a337f]]
(Apply
[a_a337f]
(TyFun [[a_a337f]] [[a_a337f]] > *)
(Let6989586621679736980InterleaveSym4
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33hh)
arg_a33hi)
(bound at Bug.hs:1295:35)
sR :: Sing [[a_a337f]] arg_a33hi (bound at Bug.hs:1287:45)
sXs :: Sing [a_a337f] arg_a33hh (bound at Bug.hs:1287:41)
sInterleave' :: forall (arg_a33he :: TyFun
[a_a337f] c69895866216793215480
> *) (arg_a33hf :: [a_a337f]) (arg_a33hg :: [c69895866216793215480]).
Sing (TyFun [a_a337f] c69895866216793215480 > *) arg_a33he
> Sing [a_a337f] arg_a33hf
> Sing [c69895866216793215480] arg_a33hg
> Sing
([a_a337f], [c69895866216793215480])
(Apply
[c69895866216793215480]
([a_a337f], [c69895866216793215480])
(Apply
[a_a337f]
([c69895866216793215480] ~> ([a_a337f], [c69895866216793215480]))
(Apply
(TyFun [a_a337f] c69895866216793215480 > *)
([a_a337f]
~> ([c69895866216793215480]
~> ([a_a337f], [c69895866216793215480])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
c69895866216793215480
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33he)
arg_a33hf)
arg_a33hg)
(bound at Bug.hs:1166:29)
lambda_a33ha :: Sing a_a337f t_a33aL
> Sing [a_a337f] ts_a33aM
> Sing [a_a337f] is_a33aO
> Sing
[[a_a337f]]
(Apply
[a_a337f]
[[a_a337f]]
(Apply
[a_a337f]
([a_a337f] ~> [[a_a337f]])
(Let6989586621679736931PermsSym1 a_a337f xs0_a33a0)
arg_a33h0)
arg_a33h1)
(bound at Bug.hs:1153:23)
sTs :: Sing [a_a337f] n_a1kQd (bound at Bug.hs:1143:34)
sT :: Sing a_a337f n_a1kQc (bound at Bug.hs:1143:31)
lambda_a33gY :: Sing [a_a337f] xs0_a33a0
> Sing
[[a_a337f]]
(Apply [a_a337f] [[a_a337f]] (PermutationsSym0 a_a337f) t_a33gX)
(bound at Bug.hs:1127:11)
(Some bindings suppressed; use fmaxrelevantbinds=N or fnomaxrelevantbinds)

1328  sInterleave'))
 ^^^^^^^^^^^^
Bug.hs:1328:59: error:
• Could not deduce: (Let6989586621679736980Interleave'
[a_a337f]
[a_a337f]
a_a337f
c69895866216793215480
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO
t
t1
t2 :: ([a_a337f], [c69895866216793215480]))
~~
(Let6989586621679736980Interleave'
[a_a337f]
[a_a337f]
a_a337f
[a_a337f]
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO
t
t1
t2 :: ([a_a337f], [c69895866216793215480]))
from the context: t_a33gX ~ xs0_a33a0
bound by the type signature for:
lambda_a33gY :: forall (xs0_a33a0 :: [a_a337f]).
t_a33gX ~ xs0_a33a0 =>
Sing [a_a337f] xs0_a33a0
> Sing
[[a_a337f]]
(Apply
[a_a337f] [[a_a337f]] (PermutationsSym0 a_a337f) t_a33gX)
at Bug.hs:(1122,11)(1126,67)
or from: arg_a33h0 ~ (':) a_a337f n_a1kQc n_a1kQd
bound by a pattern with constructor:
SCons :: forall a_11 (z_a1kQb :: [a_11]) (n_a1kQc :: a_11) (n_a1kQd :: [a_11]).
z_a1kQb ~ (':) a_11 n_a1kQc n_a1kQd =>
Sing a_11 n_a1kQc > Sing [a_11] n_a1kQd > Sing [a_11] z_a1kQb,
in an equation for ‘sPerms’
at Bug.hs:1143:2536
or from: (arg_a33h0
~
Apply
[a_a337f]
[a_a337f]
(Apply
a_a337f (TyFun [a_a337f] [a_a337f] > *) ((:$) a_a337f) t_a33aL)
ts_a33aM,
arg_a33h1 ~ is_a33aO)
bound by the type signature for:
lambda_a33ha :: forall (t_a33aL :: a_a337f) (ts_a33aM :: [a_a337f]) (is_a33aO :: [a_a337f]).
(arg_a33h0
~
Apply
[a_a337f]
[a_a337f]
(Apply
a_a337f
(TyFun [a_a337f] [a_a337f] > *)
((:$) a_a337f)
t_a33aL)
ts_a33aM,
arg_a33h1 ~ is_a33aO) =>
Sing a_a337f t_a33aL
> Sing [a_a337f] ts_a33aM
> Sing [a_a337f] is_a33aO
> Sing
[[a_a337f]]
(Apply
[a_a337f]
[[a_a337f]]
(Apply
[a_a337f]
([a_a337f] ~> [[a_a337f]])
(Let6989586621679736931PermsSym1 a_a337f xs0_a33a0)
arg_a33h0)
arg_a33h1)
at Bug.hs:(1145,23)(1152,117)
or from: (arg_a33hh ~ xs_a33fp, arg_a33hi ~ r_a33fq)
bound by the type signature for:
lambda_a33iH :: forall (xs_a33fp :: [a_a337f]) (r_a33fq :: [[a_a337f]]).
(arg_a33hh ~ xs_a33fp, arg_a33hi ~ r_a33fq) =>
Sing [a_a337f] xs_a33fp
> Sing [[a_a337f]] r_a33fq
> Sing
[[a_a337f]]
(Apply
[[a_a337f]]
[[a_a337f]]
(Apply
[a_a337f]
(TyFun [[a_a337f]] [[a_a337f]] > *)
(Let6989586621679736980InterleaveSym4
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33hh)
arg_a33hi)
at Bug.hs:(1289,35)(1294,157)
Expected type: Sing (TyFun [a_a337f] [a_a337f] > *) t
> Sing [a_a337f] t1
> Sing [[a_a337f]] t2
> Sing
([a_a337f], [[a_a337f]])
((@@)
[[a_a337f]]
([a_a337f], [[a_a337f]])
((@@)
[a_a337f]
([[a_a337f]] ~> ([a_a337f], [[a_a337f]]))
((@@)
(TyFun [a_a337f] [a_a337f] > *)
([a_a337f] ~> ([[a_a337f]] ~> ([a_a337f], [[a_a337f]])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
[a_a337f]
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
t)
t1)
t2)
Actual type: Sing (TyFun [a_a337f] c69895866216793215480 > *) t
> Sing [a_a337f] t1
> Sing [c69895866216793215480] t2
> Sing
([a_a337f], [c69895866216793215480])
(Apply
[c69895866216793215480]
([a_a337f], [c69895866216793215480])
(Apply
[a_a337f]
([c69895866216793215480] ~> ([a_a337f], [c69895866216793215480]))
(Apply
(TyFun [a_a337f] c69895866216793215480 > *)
([a_a337f]
~> ([c69895866216793215480]
~> ([a_a337f], [c69895866216793215480])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
c69895866216793215480
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
t)
t1)
t2)
The type variable ‘c69895866216793215480’ is ambiguous
• In the second argument of ‘singFun3’, namely ‘sInterleave'’
In the first argument of ‘applySing’, namely
‘((singFun3
(Proxy ::
Proxy (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO)))
sInterleave')’
In the first argument of ‘applySing’, namely
‘((applySing
((singFun3
(Proxy ::
Proxy (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO)))
sInterleave'))
((singFun1 (Proxy :: Proxy IdSym0)) sId))’
• Relevant bindings include
sX_6989586621679737266 :: Sing
([a_a337f], [[a_a337f]])
(Let6989586621679737265X_6989586621679737266Sym6
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO
xs_a33fp
r_a33fq)
(bound at Bug.hs:1321:41)
r_a33iK :: Sing [[a_a337f]] r_a33fq (bound at Bug.hs:1295:57)
xs_a33iJ :: Sing [a_a337f] xs_a33fp (bound at Bug.hs:1295:48)
lambda_a33iH :: Sing [a_a337f] xs_a33fp
> Sing [[a_a337f]] r_a33fq
> Sing
[[a_a337f]]
(Apply
[[a_a337f]]
[[a_a337f]]
(Apply
[a_a337f]
(TyFun [[a_a337f]] [[a_a337f]] > *)
(Let6989586621679736980InterleaveSym4
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33hh)
arg_a33hi)
(bound at Bug.hs:1295:35)
sR :: Sing [[a_a337f]] arg_a33hi (bound at Bug.hs:1287:45)
sXs :: Sing [a_a337f] arg_a33hh (bound at Bug.hs:1287:41)
sInterleave' :: forall (arg_a33he :: TyFun
[a_a337f] c69895866216793215480
> *) (arg_a33hf :: [a_a337f]) (arg_a33hg :: [c69895866216793215480]).
Sing (TyFun [a_a337f] c69895866216793215480 > *) arg_a33he
> Sing [a_a337f] arg_a33hf
> Sing [c69895866216793215480] arg_a33hg
> Sing
([a_a337f], [c69895866216793215480])
(Apply
[c69895866216793215480]
([a_a337f], [c69895866216793215480])
(Apply
[a_a337f]
([c69895866216793215480] ~> ([a_a337f], [c69895866216793215480]))
(Apply
(TyFun [a_a337f] c69895866216793215480 > *)
([a_a337f]
~> ([c69895866216793215480]
~> ([a_a337f], [c69895866216793215480])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
c69895866216793215480
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33he)
arg_a33hf)
arg_a33hg)
(bound at Bug.hs:1166:29)
lambda_a33ha :: Sing a_a337f t_a33aL
> Sing [a_a337f] ts_a33aM
> Sing [a_a337f] is_a33aO
> Sing
[[a_a337f]]
(Apply
[a_a337f]
[[a_a337f]]
(Apply
[a_a337f]
([a_a337f] ~> [[a_a337f]])
(Let6989586621679736931PermsSym1 a_a337f xs0_a33a0)
arg_a33h0)
arg_a33h1)
(bound at Bug.hs:1153:23)
sTs :: Sing [a_a337f] n_a1kQd (bound at Bug.hs:1143:34)
sT :: Sing a_a337f n_a1kQc (bound at Bug.hs:1143:31)
lambda_a33gY :: Sing [a_a337f] xs0_a33a0
> Sing
[[a_a337f]]
(Apply [a_a337f] [[a_a337f]] (PermutationsSym0 a_a337f) t_a33gX)
(bound at Bug.hs:1127:11)
(Some bindings suppressed; use fmaxrelevantbinds=N or fnomaxrelevantbinds)

1328  sInterleave'))
 ^^^^^^^^^^^^
```8.4.1https://gitlab.haskell.org/ghc/ghc/issues/13546Kind error with type equality20190707T18:21:24ZVladislav ZavialovKind error with type equalityThis code
```hs
{# LANGUAGE TypeInType, TypeFamilies, GADTs, ConstraintKinds #}
import Data.Kind
data Dict c where
Dict :: c => Dict c
data T (t :: k)
type family UnT (a :: Type) :: k where
UnT (T t) = t
untt :: Dict (UnT (T "a") ~ "a")
untt = Dict
tunt :: Dict (T (UnT (T "a")) ~ T "a")
tunt = Dict
```
fails with this error:
```
tunt.hs:17:8: error:
• Couldn't match kind ‘k’ with ‘GHC.Types.Symbol’
‘k’ is a rigid type variable bound by
the type signature for:
tunt :: forall k. Dict T (UnT (T "a")) ~ T "a"
at tunt.hs:16:138
When matching types
UnT (T "a") :: k
"a" :: GHC.Types.Symbol
• In the expression: Dict
In an equation for ‘tunt’: tunt = Dict
• Relevant bindings include
tunt :: Dict T (UnT (T "a")) ~ T "a" (bound at tunt.hs:17:1)

17  tunt = Dict

```
Instead I would expect these reductions to take place:
```
1. T (UnT (T "a")) ~ T "a"
2. T "a" ~ T "a"
3. constraint satisfied (refl)
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  goldfire 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Kind error with type equality","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"This code\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeInType, TypeFamilies, GADTs, ConstraintKinds #}\r\n\r\nimport Data.Kind\r\n\r\ndata Dict c where\r\n Dict :: c => Dict c\r\n\r\ndata T (t :: k)\r\n\r\ntype family UnT (a :: Type) :: k where\r\n UnT (T t) = t\r\n\r\nuntt :: Dict (UnT (T \"a\") ~ \"a\")\r\nuntt = Dict\r\n\r\ntunt :: Dict (T (UnT (T \"a\")) ~ T \"a\")\r\ntunt = Dict\r\n}}}\r\n\r\nfails with this error:\r\n\r\n{{{\r\ntunt.hs:17:8: error:\r\n • Couldn't match kind ‘k’ with ‘GHC.Types.Symbol’\r\n ‘k’ is a rigid type variable bound by\r\n the type signature for:\r\n tunt :: forall k. Dict T (UnT (T \"a\")) ~ T \"a\"\r\n at tunt.hs:16:138\r\n When matching types\r\n UnT (T \"a\") :: k\r\n \"a\" :: GHC.Types.Symbol\r\n • In the expression: Dict\r\n In an equation for ‘tunt’: tunt = Dict\r\n • Relevant bindings include\r\n tunt :: Dict T (UnT (T \"a\")) ~ T \"a\" (bound at tunt.hs:17:1)\r\n \r\n17  tunt = Dict\r\n  \r\n}}}\r\n\r\nInstead I would expect these reductions to take place:\r\n\r\n{{{\r\n 1. T (UnT (T \"a\")) ~ T \"a\"\r\n 2. T \"a\" ~ T \"a\"\r\n 3. constraint satisfied (refl)\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >This code
```hs
{# LANGUAGE TypeInType, TypeFamilies, GADTs, ConstraintKinds #}
import Data.Kind
data Dict c where
Dict :: c => Dict c
data T (t :: k)
type family UnT (a :: Type) :: k where
UnT (T t) = t
untt :: Dict (UnT (T "a") ~ "a")
untt = Dict
tunt :: Dict (T (UnT (T "a")) ~ T "a")
tunt = Dict
```
fails with this error:
```
tunt.hs:17:8: error:
• Couldn't match kind ‘k’ with ‘GHC.Types.Symbol’
‘k’ is a rigid type variable bound by
the type signature for:
tunt :: forall k. Dict T (UnT (T "a")) ~ T "a"
at tunt.hs:16:138
When matching types
UnT (T "a") :: k
"a" :: GHC.Types.Symbol
• In the expression: Dict
In an equation for ‘tunt’: tunt = Dict
• Relevant bindings include
tunt :: Dict T (UnT (T "a")) ~ T "a" (bound at tunt.hs:17:1)

17  tunt = Dict

```
Instead I would expect these reductions to take place:
```
1. T (UnT (T "a")) ~ T "a"
2. T "a" ~ T "a"
3. constraint satisfied (refl)
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  goldfire 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Kind error with type equality","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"This code\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeInType, TypeFamilies, GADTs, ConstraintKinds #}\r\n\r\nimport Data.Kind\r\n\r\ndata Dict c where\r\n Dict :: c => Dict c\r\n\r\ndata T (t :: k)\r\n\r\ntype family UnT (a :: Type) :: k where\r\n UnT (T t) = t\r\n\r\nuntt :: Dict (UnT (T \"a\") ~ \"a\")\r\nuntt = Dict\r\n\r\ntunt :: Dict (T (UnT (T \"a\")) ~ T \"a\")\r\ntunt = Dict\r\n}}}\r\n\r\nfails with this error:\r\n\r\n{{{\r\ntunt.hs:17:8: error:\r\n • Couldn't match kind ‘k’ with ‘GHC.Types.Symbol’\r\n ‘k’ is a rigid type variable bound by\r\n the type signature for:\r\n tunt :: forall k. Dict T (UnT (T \"a\")) ~ T \"a\"\r\n at tunt.hs:16:138\r\n When matching types\r\n UnT (T \"a\") :: k\r\n \"a\" :: GHC.Types.Symbol\r\n • In the expression: Dict\r\n In an equation for ‘tunt’: tunt = Dict\r\n • Relevant bindings include\r\n tunt :: Dict T (UnT (T \"a\")) ~ T \"a\" (bound at tunt.hs:17:1)\r\n \r\n17  tunt = Dict\r\n  \r\n}}}\r\n\r\nInstead I would expect these reductions to take place:\r\n\r\n{{{\r\n 1. T (UnT (T \"a\")) ~ T \"a\"\r\n 2. T \"a\" ~ T \"a\"\r\n 3. constraint satisfied (refl)\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc/issues/13530Horrible error message due to TypeInType20190707T18:21:28ZSimon Peyton JonesHorrible error message due to TypeInTypeConsider this
```
{# LANGUAGE MagicHash, UnboxedTuples #}
module Foo where
import GHC.Exts
g :: Int > (# Int#, a #)
g (I# y) = (# y, undefined #)
f :: Int > (# Int#, Int# #)
f x = g x
```
With GHC 8 we get
```
Foo.hs:11:7: error:
• Couldn't match a lifted type with an unlifted type
Expected type: (# Int#, Int# #)
Actual type: (# Int#, Int# #)
```
What a terrible error message!! It was much better in GHC 7.10:
```
Foo.hs:11:7:
Couldn't match kind ‘*’ with ‘#’
When matching types
a0 :: *
Int# :: #
Expected type: (# Int#, Int# #)
Actual type: (# Int#, a0 #)
```
What's going on?
The constraint solver sees
```
[W] alpha::TYPE LiftedRep ~ Int#::TYPE IntRep
```
So it homogenises the kinds, *and unifies alpha* (this did not happen in GHC 7.10), thus
```
alpha := Int# > TYPE co
[W] co :: LiftedRep ~ IntRep
```
Of course the new constraint fails. But since we have unified alpha, when we print out the types are are unifying they both look like `(# Int#, Int# #)` (there's a suppressed cast in the second component).
I'm not sure what to do here.
(I tripped over this when debugging #13509.)Consider this
```
{# LANGUAGE MagicHash, UnboxedTuples #}
module Foo where
import GHC.Exts
g :: Int > (# Int#, a #)
g (I# y) = (# y, undefined #)
f :: Int > (# Int#, Int# #)
f x = g x
```
With GHC 8 we get
```
Foo.hs:11:7: error:
• Couldn't match a lifted type with an unlifted type
Expected type: (# Int#, Int# #)
Actual type: (# Int#, Int# #)
```
What a terrible error message!! It was much better in GHC 7.10:
```
Foo.hs:11:7:
Couldn't match kind ‘*’ with ‘#’
When matching types
a0 :: *
Int# :: #
Expected type: (# Int#, Int# #)
Actual type: (# Int#, a0 #)
```
What's going on?
The constraint solver sees
```
[W] alpha::TYPE LiftedRep ~ Int#::TYPE IntRep
```
So it homogenises the kinds, *and unifies alpha* (this did not happen in GHC 7.10), thus
```
alpha := Int# > TYPE co
[W] co :: LiftedRep ~ IntRep
```
Of course the new constraint fails. But since we have unified alpha, when we print out the types are are unifying they both look like `(# Int#, Int# #)` (there's a suppressed cast in the second component).
I'm not sure what to do here.
(I tripped over this when debugging #13509.)https://gitlab.haskell.org/ghc/ghc/issues/13409Data types with higherrank kinds are prettyprinted strangely20190707T18:22:00ZRyan ScottData types with higherrank kinds are prettyprinted strangelyFirst observed in #13399\##13409. If you define this:
```hs
data Foo :: (* > *) > (forall k. k > *)
```
and type `:i Foo` into GHCi, you get this back:
```
type role Foo phantom nominal phantom
data Foo (a :: * > *) k (c :: k)
```
This seems to imply that Foo has three visible type parameters, which isn't true at all!
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Data types with higherrank kinds are prettyprinted strangely","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.2","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"First observed in https://ghc.haskell.org/trac/ghc/ticket/13399#comment:5. If you define this:\r\n\r\n{{{#!hs\r\ndata Foo :: (* > *) > (forall k. k > *)\r\n}}}\r\n\r\nand type `:i Foo` into GHCi, you get this back:\r\n\r\n{{{\r\ntype role Foo phantom nominal phantom\r\ndata Foo (a :: * > *) k (c :: k)\r\n}}}\r\n\r\nThis seems to imply that Foo has three visible type parameters, which isn't true at all!","type_of_failure":"OtherFailure","blocking":[]} >First observed in #13399\##13409. If you define this:
```hs
data Foo :: (* > *) > (forall k. k > *)
```
and type `:i Foo` into GHCi, you get this back:
```
type role Foo phantom nominal phantom
data Foo (a :: * > *) k (c :: k)
```
This seems to imply that Foo has three visible type parameters, which isn't true at all!
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Data types with higherrank kinds are prettyprinted strangely","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.2","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"First observed in https://ghc.haskell.org/trac/ghc/ticket/13399#comment:5. If you define this:\r\n\r\n{{{#!hs\r\ndata Foo :: (* > *) > (forall k. k > *)\r\n}}}\r\n\r\nand type `:i Foo` into GHCi, you get this back:\r\n\r\n{{{\r\ntype role Foo phantom nominal phantom\r\ndata Foo (a :: * > *) k (c :: k)\r\n}}}\r\n\r\nThis seems to imply that Foo has three visible type parameters, which isn't true at all!","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc/issues/13408Consider inferring a higherrank kind for type synonyms20200123T19:31:52ZRichard Eisenbergrae@richarde.devConsider inferring a higherrank kind for type synonymsIn terms, a definition comprising one nonrecursive equation may have a higherrank type inferred. For example:
```hs
f :: (forall a. a > a > a) > Int
f z = z 0 1
g = f
```
`g` gets an inferred type equal to `f`'s. However, this fails at the type level:
```hs
type F (z :: forall a. a > a > a) = z 0 1
type G = F
```
If anything is strange here, it's that the termlevel definition is accepted. GHC should not be in the business of inferring higherrank types. But there is an exception for definitions comprising one nonrecursive equation.
This ticket proposes expanding this behavior to the type level, allowing `G` to be accepted.
This is spun off from #13399, but is not tightly coupled to that ticket.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Consider inferring a higherrank kind for type synonyms","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"In terms, a definition comprising one nonrecursive equation may have a higherrank type inferred. For example:\r\n\r\n{{{#!hs\r\nf :: (forall a. a > a > a) > Int\r\nf z = z 0 1\r\n\r\ng = f\r\n}}}\r\n\r\n`g` gets an inferred type equal to `f`'s. However, this fails at the type level:\r\n\r\n{{{#!hs\r\ntype F (z :: forall a. a > a > a) = z 0 1\r\n\r\ntype G = F\r\n}}}\r\n\r\nIf anything is strange here, it's that the termlevel definition is accepted. GHC should not be in the business of inferring higherrank types. But there is an exception for definitions comprising one nonrecursive equation.\r\n\r\nThis ticket proposes expanding this behavior to the type level, allowing `G` to be accepted.\r\n\r\nThis is spun off from #13399, but is not tightly coupled to that ticket.","type_of_failure":"OtherFailure","blocking":[]} >In terms, a definition comprising one nonrecursive equation may have a higherrank type inferred. For example:
```hs
f :: (forall a. a > a > a) > Int
f z = z 0 1
g = f
```
`g` gets an inferred type equal to `f`'s. However, this fails at the type level:
```hs
type F (z :: forall a. a > a > a) = z 0 1
type G = F
```
If anything is strange here, it's that the termlevel definition is accepted. GHC should not be in the business of inferring higherrank types. But there is an exception for definitions comprising one nonrecursive equation.
This ticket proposes expanding this behavior to the type level, allowing `G` to be accepted.
This is spun off from #13399, but is not tightly coupled to that ticket.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Consider inferring a higherrank kind for type synonyms","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"In terms, a definition comprising one nonrecursive equation may have a higherrank type inferred. For example:\r\n\r\n{{{#!hs\r\nf :: (forall a. a > a > a) > Int\r\nf z = z 0 1\r\n\r\ng = f\r\n}}}\r\n\r\n`g` gets an inferred type equal to `f`'s. However, this fails at the type level:\r\n\r\n{{{#!hs\r\ntype F (z :: forall a. a > a > a) = z 0 1\r\n\r\ntype G = F\r\n}}}\r\n\r\nIf anything is strange here, it's that the termlevel definition is accepted. GHC should not be in the business of inferring higherrank types. But there is an exception for definitions comprising one nonrecursive equation.\r\n\r\nThis ticket proposes expanding this behavior to the type level, allowing `G` to be accepted.\r\n\r\nThis is spun off from #13399, but is not tightly coupled to that ticket.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc/issues/13407Fix printing of higherrank kinds20190707T18:22:01ZRichard Eisenbergrae@richarde.devFix printing of higherrank kindsWitness this GHCi session:
```
rae:09:18:37 ~/ghc/ghc> ghci ignoredotghci
GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help
Prelude> :set XTypeInType XRankNTypes
Prelude> import Data.Kind
Prelude Data.Kind> data Foo :: (* > *) > (forall k. k > *)
Prelude Data.Kind> :info Foo
type role Foo phantom nominal phantom
data Foo (a :: * > *) k (c :: k)
 Defined at <interactive>:3:1
```
The output from `:info` is terrible, treating `k` as a visible parameter when it isn't.
This is spun off from #13399 but is not tightly coupled to that ticket.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 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":"Fix printing of higherrank kinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Witness this GHCi session:\r\n\r\n{{{\r\nrae:09:18:37 ~/ghc/ghc> ghci ignoredotghci\r\nGHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help\r\nPrelude> :set XTypeInType XRankNTypes\r\nPrelude> import Data.Kind\r\nPrelude Data.Kind> data Foo :: (* > *) > (forall k. k > *)\r\nPrelude Data.Kind> :info Foo\r\ntype role Foo phantom nominal phantom\r\ndata Foo (a :: * > *) k (c :: k)\r\n \t Defined at <interactive>:3:1\r\n}}}\r\n\r\nThe output from `:info` is terrible, treating `k` as a visible parameter when it isn't.\r\n\r\nThis is spun off from #13399 but is not tightly coupled to that ticket.","type_of_failure":"OtherFailure","blocking":[]} >Witness this GHCi session:
```
rae:09:18:37 ~/ghc/ghc> ghci ignoredotghci
GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help
Prelude> :set XTypeInType XRankNTypes
Prelude> import Data.Kind
Prelude Data.Kind> data Foo :: (* > *) > (forall k. k > *)
Prelude Data.Kind> :info Foo
type role Foo phantom nominal phantom
data Foo (a :: * > *) k (c :: k)
 Defined at <interactive>:3:1
```
The output from `:info` is terrible, treating `k` as a visible parameter when it isn't.
This is spun off from #13399 but is not tightly coupled to that ticket.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 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":"Fix printing of higherrank kinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Witness this GHCi session:\r\n\r\n{{{\r\nrae:09:18:37 ~/ghc/ghc> ghci ignoredotghci\r\nGHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help\r\nPrelude> :set XTypeInType XRankNTypes\r\nPrelude> import Data.Kind\r\nPrelude Data.Kind> data Foo :: (* > *) > (forall k. k > *)\r\nPrelude Data.Kind> :info Foo\r\ntype role Foo phantom nominal phantom\r\ndata Foo (a :: * > *) k (c :: k)\r\n \t Defined at <interactive>:3:1\r\n}}}\r\n\r\nThe output from `:info` is terrible, treating `k` as a visible parameter when it isn't.\r\n\r\nThis is spun off from #13399 but is not tightly coupled to that ticket.","type_of_failure":"OtherFailure","blocking":[]} >8.4.1https://gitlab.haskell.org/ghc/ghc/issues/13399Location of `forall` matters with higherrank kind polymorphism20190707T18:22:03ZEric CrockettLocation of `forall` matters with higherrank kind polymorphismThe following code fails to compile, but probably should:
```hs
{# LANGUAGE RankNTypes, TypeInType #}
import Data.Kind
data Foo :: forall k . (* > *) > k > *  Decl 1
class C (a :: forall k . k > *)
instance C (Foo a)  error on this line
```
with the error
```
• Expected kind ‘forall k. k > *’, but ‘Foo a’ has kind ‘k0 > *’
• In the first argument of ‘C’, namely ‘Foo a’
In the instance declaration for ‘C (Foo a)’
```
Similarly, the following declarations of `Foo` also cause a similar error at the instance declaration:
Decl 2: `data Foo :: (* > *) > k > *`
Decl 3: `data Foo (a :: * > *) (b :: k)`
However, if I move the `forall` to a point *after* the first type parameter (which is where the instance is partially applied) thusly:
Decl 4: `data Foo :: (* > *) > forall k . k > *`
then GHC happily accepts the instance of `C`.
From my (admittedly negligible) knowledge of type theory, the signatures for Decls 1 and 4 (and 2) are identical, since the `forall` can be floated to the front of Decl 4. GHC should accept any of the four versions of `Foo`, since they are all equivalent.The following code fails to compile, but probably should:
```hs
{# LANGUAGE RankNTypes, TypeInType #}
import Data.Kind
data Foo :: forall k . (* > *) > k > *  Decl 1
class C (a :: forall k . k > *)
instance C (Foo a)  error on this line
```
with the error
```
• Expected kind ‘forall k. k > *’, but ‘Foo a’ has kind ‘k0 > *’
• In the first argument of ‘C’, namely ‘Foo a’
In the instance declaration for ‘C (Foo a)’
```
Similarly, the following declarations of `Foo` also cause a similar error at the instance declaration:
Decl 2: `data Foo :: (* > *) > k > *`
Decl 3: `data Foo (a :: * > *) (b :: k)`
However, if I move the `forall` to a point *after* the first type parameter (which is where the instance is partially applied) thusly:
Decl 4: `data Foo :: (* > *) > forall k . k > *`
then GHC happily accepts the instance of `C`.
From my (admittedly negligible) knowledge of type theory, the signatures for Decls 1 and 4 (and 2) are identical, since the `forall` can be floated to the front of Decl 4. GHC should accept any of the four versions of `Foo`, since they are all equivalent.8.4.1https://gitlab.haskell.org/ghc/ghc/issues/13391PolyKinds is more permissive in GHC 820190707T18:22:06ZEric CrockettPolyKinds is more permissive in GHC 8The docs claim that the definition in section 9.11.10
```
data G (a :: k) where
GInt :: G Int
GMaybe :: G Maybe
```
"requires that `XTypeInType` be in effect", but this isn't the case.
The following compiles with GHC8.0.2:
```
{# LANGUAGE PolyKinds, GADTs #}
data G (a :: k) where
GInt :: G Int
GMaybe :: G Maybe
```
The example does \*not\* compile with 7.10.3, so this seems to be a case where `XPolyKinds` has become more permissive in GHC 8 (as outlined in section 9.11.1).
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.2 
 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":"PolyKinds is more permissive in GHC 8","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The docs claim that the definition in section 9.11.10\r\n\r\n{{{\r\ndata G (a :: k) where\r\n GInt :: G Int\r\n GMaybe :: G Maybe\r\n}}}\r\n\r\n\"requires that `XTypeInType` be in effect\", but this isn't the case.\r\n\r\nThe following compiles with GHC8.0.2:\r\n\r\n{{{\r\n\r\n{# LANGUAGE PolyKinds, GADTs #}\r\n\r\ndata G (a :: k) where\r\n GInt :: G Int\r\n GMaybe :: G Maybe\r\n}}}\r\n\r\nThe example does *not* compile with 7.10.3, so this seems to be a case where `XPolyKinds` has become more permissive in GHC 8 (as outlined in section 9.11.1). ","type_of_failure":"OtherFailure","blocking":[]} >The docs claim that the definition in section 9.11.10
```
data G (a :: k) where
GInt :: G Int
GMaybe :: G Maybe
```
"requires that `XTypeInType` be in effect", but this isn't the case.
The following compiles with GHC8.0.2:
```
{# LANGUAGE PolyKinds, GADTs #}
data G (a :: k) where
GInt :: G Int
GMaybe :: G Maybe
```
The example does \*not\* compile with 7.10.3, so this seems to be a case where `XPolyKinds` has become more permissive in GHC 8 (as outlined in section 9.11.1).
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.2 
 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":"PolyKinds is more permissive in GHC 8","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The docs claim that the definition in section 9.11.10\r\n\r\n{{{\r\ndata G (a :: k) where\r\n GInt :: G Int\r\n GMaybe :: G Maybe\r\n}}}\r\n\r\n\"requires that `XTypeInType` be in effect\", but this isn't the case.\r\n\r\nThe following compiles with GHC8.0.2:\r\n\r\n{{{\r\n\r\n{# LANGUAGE PolyKinds, GADTs #}\r\n\r\ndata G (a :: k) where\r\n GInt :: G Int\r\n GMaybe :: G Maybe\r\n}}}\r\n\r\nThe example does *not* compile with 7.10.3, so this seems to be a case where `XPolyKinds` has become more permissive in GHC 8 (as outlined in section 9.11.1). ","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc/issues/13364Remove checkValidTelescope20190707T18:22:16ZRichard Eisenbergrae@richarde.devRemove checkValidTelescopeAll of this new `TypeInType` nonsense has provided a number of ways that we can arrive at illscoped kinds. Let's assume we have
```
data SameKind :: k > k > Type
```
and then here are three subtly illscoped kinds:
```
forall a (b :: a) (c :: Proxy d). SameKind b d
forall a. forall (b :: a). forall (c :: Proxy d). SameKind b d
forall d. forall a (b :: a). SameKind b d
```
Despite the close similarity between these cases, they are all handled separately. See `Note [Bad telescopes]` in !TcValidity for an overview, but these are spread between `tcImplicitTKBndrsX`, `tcExplicitTKBndrsX`, and those functions' calls to `checkValidTelescope`, `checkZonkValidTelescope`, and `checkValidInferredKinds`.
While I am unaware of a concrete bug this all causes, it's a mess.
Better would be to use the existing machinery to prevent skolemescape: `TcLevel`s and implication constraints. Specifically, it's quite plausible that all this can be avoided by a simple rule: bump the `TcLevel` (and create an implication constraint) for *every* new type variable brought into scope (including implicitly). (Actually, implicit variables have an implicit ordering that GHC is free to decide, so all implicitly bound variables should be brought into scope at once, with just one bump in the `TcLevel`.)
It might all just work! And then we can delete gobs of hairy code. Hooray!
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Task 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Remove checkValidTelescope","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"All of this new `TypeInType` nonsense has provided a number of ways that we can arrive at illscoped kinds. Let's assume we have\r\n\r\n{{{\r\ndata SameKind :: k > k > Type\r\n}}}\r\n\r\nand then here are three subtly illscoped kinds:\r\n\r\n{{{\r\nforall a (b :: a) (c :: Proxy d). SameKind b d\r\nforall a. forall (b :: a). forall (c :: Proxy d). SameKind b d\r\nforall d. forall a (b :: a). SameKind b d\r\n}}}\r\n\r\nDespite the close similarity between these cases, they are all handled separately. See `Note [Bad telescopes]` in !TcValidity for an overview, but these are spread between `tcImplicitTKBndrsX`, `tcExplicitTKBndrsX`, and those functions' calls to `checkValidTelescope`, `checkZonkValidTelescope`, and `checkValidInferredKinds`.\r\n\r\nWhile I am unaware of a concrete bug this all causes, it's a mess.\r\n\r\nBetter would be to use the existing machinery to prevent skolemescape: `TcLevel`s and implication constraints. Specifically, it's quite plausible that all this can be avoided by a simple rule: bump the `TcLevel` (and create an implication constraint) for ''every'' new type variable brought into scope (including implicitly). (Actually, implicit variables have an implicit ordering that GHC is free to decide, so all implicitly bound variables should be brought into scope at once, with just one bump in the `TcLevel`.)\r\n\r\nIt might all just work! And then we can delete gobs of hairy code. Hooray!","type_of_failure":"OtherFailure","blocking":[]} >All of this new `TypeInType` nonsense has provided a number of ways that we can arrive at illscoped kinds. Let's assume we have
```
data SameKind :: k > k > Type
```
and then here are three subtly illscoped kinds:
```
forall a (b :: a) (c :: Proxy d). SameKind b d
forall a. forall (b :: a). forall (c :: Proxy d). SameKind b d
forall d. forall a (b :: a). SameKind b d
```
Despite the close similarity between these cases, they are all handled separately. See `Note [Bad telescopes]` in !TcValidity for an overview, but these are spread between `tcImplicitTKBndrsX`, `tcExplicitTKBndrsX`, and those functions' calls to `checkValidTelescope`, `checkZonkValidTelescope`, and `checkValidInferredKinds`.
While I am unaware of a concrete bug this all causes, it's a mess.
Better would be to use the existing machinery to prevent skolemescape: `TcLevel`s and implication constraints. Specifically, it's quite plausible that all this can be avoided by a simple rule: bump the `TcLevel` (and create an implication constraint) for *every* new type variable brought into scope (including implicitly). (Actually, implicit variables have an implicit ordering that GHC is free to decide, so all implicitly bound variables should be brought into scope at once, with just one bump in the `TcLevel`.)
It might all just work! And then we can delete gobs of hairy code. Hooray!
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Task 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Remove checkValidTelescope","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"All of this new `TypeInType` nonsense has provided a number of ways that we can arrive at illscoped kinds. Let's assume we have\r\n\r\n{{{\r\ndata SameKind :: k > k > Type\r\n}}}\r\n\r\nand then here are three subtly illscoped kinds:\r\n\r\n{{{\r\nforall a (b :: a) (c :: Proxy d). SameKind b d\r\nforall a. forall (b :: a). forall (c :: Proxy d). SameKind b d\r\nforall d. forall a (b :: a). SameKind b d\r\n}}}\r\n\r\nDespite the close similarity between these cases, they are all handled separately. See `Note [Bad telescopes]` in !TcValidity for an overview, but these are spread between `tcImplicitTKBndrsX`, `tcExplicitTKBndrsX`, and those functions' calls to `checkValidTelescope`, `checkZonkValidTelescope`, and `checkValidInferredKinds`.\r\n\r\nWhile I am unaware of a concrete bug this all causes, it's a mess.\r\n\r\nBetter would be to use the existing machinery to prevent skolemescape: `TcLevel`s and implication constraints. Specifically, it's quite plausible that all this can be avoided by a simple rule: bump the `TcLevel` (and create an implication constraint) for ''every'' new type variable brought into scope (including implicitly). (Actually, implicit variables have an implicit ordering that GHC is free to decide, so all implicitly bound variables should be brought into scope at once, with just one bump in the `TcLevel`.)\r\n\r\nIt might all just work! And then we can delete gobs of hairy code. Hooray!","type_of_failure":"OtherFailure","blocking":[]} >8.4.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/issues/13337GHC doesn't think a type is of kind *, despite having evidence for it20190707T18:22:23ZRyan ScottGHC doesn't think a type is of kind *, despite having evidence for itThe easiest way to illustrate this bug is this:
```hs
{# LANGUAGE PolyKinds #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
module Foo where
import Data.Kind (Type)
blah :: forall (a :: k). k ~ Type => a > a
blah x = x
```
```
$ ghci Foo.hs
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo ( Foo.hs, interpreted )
Foo.hs:8:43: error:
• Expected a type, but ‘a’ has kind ‘k’
• In the type signature:
blah :: forall (a :: k). k ~ Type => a > a
```
I find this behavior quite surprising, especially since we have evidence that `k ~ Type` in scope!
If the program above looks too contrived, consider a similar program that uses `Typeable`. I want to write something like this:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Foo where
import Data.Kind (Type)
import Data.Typeable
foo :: forall k (a :: k) proxy. (Typeable k, Typeable a)
=> proxy a > String
foo _ =
case eqT :: Maybe (k :~: Type) of
Nothing > "NonType kind"
Just Refl >
case eqT :: Maybe (a :~: Int) of
Nothing > "NonInt type"
Just Refl > "It's an Int!"
```
This exhibits the same problem. Despite the fact that we patternmatched on a `Refl` of type `k :~: Type`, GHC refuses to consider the possibility that `a :~: Int` is well kinded, even though `(a :: k)`, and we learned from the first `Refl` that `k ~ Type`!
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  goldfire 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC doesn't think a type is of kind *, despite having evidence for it","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"The easiest way to illustrate this bug is this:\r\n\r\n{{{#!hs\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeFamilies #}\r\nmodule Foo where\r\n\r\nimport Data.Kind (Type)\r\n\r\nblah :: forall (a :: k). k ~ Type => a > a\r\nblah x = x\r\n}}}\r\n\r\n{{{\r\n$ ghci Foo.hs\r\nGHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Foo ( Foo.hs, interpreted )\r\n\r\nFoo.hs:8:43: error:\r\n • Expected a type, but ‘a’ has kind ‘k’\r\n • In the type signature:\r\n blah :: forall (a :: k). k ~ Type => a > a\r\n}}}\r\n\r\nI find this behavior quite surprising, especially since we have evidence that `k ~ Type` in scope!\r\n\r\nIf the program above looks too contrived, consider a similar program that uses `Typeable`. I want to write something like this:\r\n\r\n{{{#!hs\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Foo where\r\n\r\nimport Data.Kind (Type)\r\nimport Data.Typeable\r\n\r\nfoo :: forall k (a :: k) proxy. (Typeable k, Typeable a)\r\n => proxy a > String\r\nfoo _ =\r\n case eqT :: Maybe (k :~: Type) of\r\n Nothing > \"NonType kind\"\r\n Just Refl >\r\n case eqT :: Maybe (a :~: Int) of\r\n Nothing > \"NonInt type\"\r\n Just Refl > \"It's an Int!\"\r\n}}}\r\n\r\nThis exhibits the same problem. Despite the fact that we patternmatched on a `Refl` of type `k :~: Type`, GHC refuses to consider the possibility that `a :~: Int` is well kinded, even though `(a :: k)`, and we learned from the first `Refl` that `k ~ Type`!","type_of_failure":"OtherFailure","blocking":[]} >The easiest way to illustrate this bug is this:
```hs
{# LANGUAGE PolyKinds #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
module Foo where
import Data.Kind (Type)
blah :: forall (a :: k). k ~ Type => a > a
blah x = x
```
```
$ ghci Foo.hs
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo ( Foo.hs, interpreted )
Foo.hs:8:43: error:
• Expected a type, but ‘a’ has kind ‘k’
• In the type signature:
blah :: forall (a :: k). k ~ Type => a > a
```
I find this behavior quite surprising, especially since we have evidence that `k ~ Type` in scope!
If the program above looks too contrived, consider a similar program that uses `Typeable`. I want to write something like this:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Foo where
import Data.Kind (Type)
import Data.Typeable
foo :: forall k (a :: k) proxy. (Typeable k, Typeable a)
=> proxy a > String
foo _ =
case eqT :: Maybe (k :~: Type) of
Nothing > "NonType kind"
Just Refl >
case eqT :: Maybe (a :~: Int) of
Nothing > "NonInt type"
Just Refl > "It's an Int!"
```
This exhibits the same problem. Despite the fact that we patternmatched on a `Refl` of type `k :~: Type`, GHC refuses to consider the possibility that `a :~: Int` is well kinded, even though `(a :: k)`, and we learned from the first `Refl` that `k ~ Type`!
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  goldfire 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC doesn't think a type is of kind *, despite having evidence for it","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"The easiest way to illustrate this bug is this:\r\n\r\n{{{#!hs\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeFamilies #}\r\nmodule Foo where\r\n\r\nimport Data.Kind (Type)\r\n\r\nblah :: forall (a :: k). k ~ Type => a > a\r\nblah x = x\r\n}}}\r\n\r\n{{{\r\n$ ghci Foo.hs\r\nGHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Foo ( Foo.hs, interpreted )\r\n\r\nFoo.hs:8:43: error:\r\n • Expected a type, but ‘a’ has kind ‘k’\r\n • In the type signature:\r\n blah :: forall (a :: k). k ~ Type => a > a\r\n}}}\r\n\r\nI find this behavior quite surprising, especially since we have evidence that `k ~ Type` in scope!\r\n\r\nIf the program above looks too contrived, consider a similar program that uses `Typeable`. I want to write something like this:\r\n\r\n{{{#!hs\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Foo where\r\n\r\nimport Data.Kind (Type)\r\nimport Data.Typeable\r\n\r\nfoo :: forall k (a :: k) proxy. (Typeable k, Typeable a)\r\n => proxy a > String\r\nfoo _ =\r\n case eqT :: Maybe (k :~: Type) of\r\n Nothing > \"NonType kind\"\r\n Just Refl >\r\n case eqT :: Maybe (a :~: Int) of\r\n Nothing > \"NonInt type\"\r\n Just Refl > \"It's an Int!\"\r\n}}}\r\n\r\nThis exhibits the same problem. Despite the fact that we patternmatched on a `Refl` of type `k :~: Type`, GHC refuses to consider the possibility that `a :~: Int` is well kinded, even though `(a :: k)`, and we learned from the first `Refl` that `k ~ Type`!","type_of_failure":"OtherFailure","blocking":[]} >8.2.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/issues/13333Typeable regression in GHC HEAD20190707T18:22:24ZRyan ScottTypeable regression in GHC HEADI recently wrote some code while exploring a fix for #13327 that heavily uses polykinded `Typeable`. This compiles without issue on GHC 8.0.1 and 8.0.2:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE GADTs #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module DataCast where
import Data.Data
import GHC.Exts (Constraint)
data T (phantom :: k) = T
data D (p :: k > Constraint) (x :: j) where
D :: forall (p :: k > Constraint) (x :: k). p x => D p x
class Possibly p x where
possibly :: proxy1 p > proxy2 x > Maybe (D p x)
dataCast1T :: forall k c t (phantom :: k).
(Typeable k, Typeable t, Typeable phantom, Possibly Data phantom)
=> (forall d. Data d => c (t d))
> Maybe (c (T phantom))
dataCast1T f = case possibly (Proxy :: Proxy Data) (Proxy :: Proxy phantom) of
Nothing > Nothing
Just D > gcast1 f
```
But on GHC HEAD, it barfs this error:
```
$ ~/Software/ghc2/inplace/bin/ghcstage2 interactive Bug.hs
GHCi, version 8.1.20170223: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling DataCast ( Bug.hs, interpreted )
Bug.hs:28:29: error:
• Could not deduce (Typeable T) arising from a use of ‘gcast1’
GHC can't yet do polykinded Typeable (T :: * > *)
from the context: (Typeable k, Typeable t, Typeable phantom,
Possibly Data phantom)
bound by the type signature for:
dataCast1T :: (Typeable k, Typeable t, Typeable phantom,
Possibly Data phantom) =>
(forall d. Data d => c (t d)) > Maybe (c (T phantom))
at Bug.hs:(22,1)(25,35)
or from: (k ~ *, (phantom :: k) ~~ (x :: *), Data x)
bound by a pattern with constructor:
D :: forall k (p :: k > Constraint) (x :: k). p x => D p x,
in a case alternative
at Bug.hs:28:23
• In the expression: gcast1 f
In a case alternative: Just D > gcast1 f
In the expression:
case possibly (Proxy :: Proxy Data) (Proxy :: Proxy phantom) of
Nothing > Nothing
Just D > gcast1 f

28  Just D > gcast1 f
 ^^^^^^^^
```
That error message itself is hilariously strange, since GHC certainly has the power to do polykinded `Typeable` nowadays.
Marking as high priority since this is a regression—feel free to lower the priority if you disagree.I recently wrote some code while exploring a fix for #13327 that heavily uses polykinded `Typeable`. This compiles without issue on GHC 8.0.1 and 8.0.2:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE GADTs #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module DataCast where
import Data.Data
import GHC.Exts (Constraint)
data T (phantom :: k) = T
data D (p :: k > Constraint) (x :: j) where
D :: forall (p :: k > Constraint) (x :: k). p x => D p x
class Possibly p x where
possibly :: proxy1 p > proxy2 x > Maybe (D p x)
dataCast1T :: forall k c t (phantom :: k).
(Typeable k, Typeable t, Typeable phantom, Possibly Data phantom)
=> (forall d. Data d => c (t d))
> Maybe (c (T phantom))
dataCast1T f = case possibly (Proxy :: Proxy Data) (Proxy :: Proxy phantom) of
Nothing > Nothing
Just D > gcast1 f
```
But on GHC HEAD, it barfs this error:
```
$ ~/Software/ghc2/inplace/bin/ghcstage2 interactive Bug.hs
GHCi, version 8.1.20170223: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling DataCast ( Bug.hs, interpreted )
Bug.hs:28:29: error:
• Could not deduce (Typeable T) arising from a use of ‘gcast1’
GHC can't yet do polykinded Typeable (T :: * > *)
from the context: (Typeable k, Typeable t, Typeable phantom,
Possibly Data phantom)
bound by the type signature for:
dataCast1T :: (Typeable k, Typeable t, Typeable phantom,
Possibly Data phantom) =>
(forall d. Data d => c (t d)) > Maybe (c (T phantom))
at Bug.hs:(22,1)(25,35)
or from: (k ~ *, (phantom :: k) ~~ (x :: *), Data x)
bound by a pattern with constructor:
D :: forall k (p :: k > Constraint) (x :: k). p x => D p x,
in a case alternative
at Bug.hs:28:23
• In the expression: gcast1 f
In a case alternative: Just D > gcast1 f
In the expression:
case possibly (Proxy :: Proxy Data) (Proxy :: Proxy phantom) of
Nothing > Nothing
Just D > gcast1 f

28  Just D > gcast1 f
 ^^^^^^^^
```
That error message itself is hilariously strange, since GHC certainly has the power to do polykinded `Typeable` nowadays.
Marking as high priority since this is a regression—feel free to lower the priority if you disagree.8.2.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/issues/12938Polykinded associated type family rejected on false pretenses20190707T18:24:33ZRichard Eisenbergrae@richarde.devPolykinded associated type family rejected on false pretensesIf I say
```
class HasRep a where
type Rep a :: TYPE r
```
I get
```
• Kind variable ‘r’ is implicitly bound in datatype
‘Rep’, but does not appear as the kind of any
of its type variables. Perhaps you meant
to bind it (with TypeInType) explicitly somewhere?
Type variables with inferred kinds: a
• In the class declaration for ‘HasRep’
```
This definition should be accepted, though, as `r` is just an invisible parameter to the associated type family. (I don't know how *useful* this is, but it's not bogus.)
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 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":"Polykinded associated type family rejected on false pretenses","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If I say\r\n\r\n{{{\r\nclass HasRep a where\r\n type Rep a :: TYPE r\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\n • Kind variable ‘r’ is implicitly bound in datatype\r\n ‘Rep’, but does not appear as the kind of any\r\n of its type variables. Perhaps you meant\r\n to bind it (with TypeInType) explicitly somewhere?\r\n Type variables with inferred kinds: a\r\n • In the class declaration for ‘HasRep’\r\n}}}\r\n\r\nThis definition should be accepted, though, as `r` is just an invisible parameter to the associated type family. (I don't know how ''useful'' this is, but it's not bogus.)","type_of_failure":"OtherFailure","blocking":[]} >If I say
```
class HasRep a where
type Rep a :: TYPE r
```
I get
```
• Kind variable ‘r’ is implicitly bound in datatype
‘Rep’, but does not appear as the kind of any
of its type variables. Perhaps you meant
to bind it (with TypeInType) explicitly somewhere?
Type variables with inferred kinds: a
• In the class declaration for ‘HasRep’
```
This definition should be accepted, though, as `r` is just an invisible parameter to the associated type family. (I don't know how *useful* this is, but it's not bogus.)
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 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":"Polykinded associated type family rejected on false pretenses","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If I say\r\n\r\n{{{\r\nclass HasRep a where\r\n type Rep a :: TYPE r\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\n • Kind variable ‘r’ is implicitly bound in datatype\r\n ‘Rep’, but does not appear as the kind of any\r\n of its type variables. Perhaps you meant\r\n to bind it (with TypeInType) explicitly somewhere?\r\n Type variables with inferred kinds: a\r\n • In the class declaration for ‘HasRep’\r\n}}}\r\n\r\nThis definition should be accepted, though, as `r` is just an invisible parameter to the associated type family. (I don't know how ''useful'' this is, but it's not bogus.)","type_of_failure":"OtherFailure","blocking":[]} >8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.dev