GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2020-09-19T19:52:25Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/12081TypeInType Compile-time Panic2020-09-19T19:52:25ZMichaelKTypeInType Compile-time PanicI've been playing around with GHC 8.0.1-rc4 release and got a panic from the following (stripped down) code:
```hs
{-# LANGUAGE TypeInType #-}
data Nat = Z | S Nat
class C (n :: Nat) where
type T n :: Nat
f :: (a :: T n)
```
```
ghc: panic! (the 'impossible' happened)
(GHC version 8.0.0.20160421 for x86_64-apple-darwin):
isInjectiveTyCon sees a TcTyCon T
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1-rc4 |
| 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":"TypeInType Compile-time Panic","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc4","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I've been playing around with GHC 8.0.1-rc4 release and got a panic from the following (stripped down) code:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeInType #-}\r\n\r\ndata Nat = Z | S Nat\r\n\r\nclass C (n :: Nat) where\r\n type T n :: Nat\r\n f :: (a :: T n)\r\n}}}\r\n\r\n{{{\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.0.0.20160421 for x86_64-apple-darwin):\r\n\tisInjectiveTyCon sees a TcTyCon T\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->I've been playing around with GHC 8.0.1-rc4 release and got a panic from the following (stripped down) code:
```hs
{-# LANGUAGE TypeInType #-}
data Nat = Z | S Nat
class C (n :: Nat) where
type T n :: Nat
f :: (a :: T n)
```
```
ghc: panic! (the 'impossible' happened)
(GHC version 8.0.0.20160421 for x86_64-apple-darwin):
isInjectiveTyCon sees a TcTyCon T
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1-rc4 |
| 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":"TypeInType Compile-time Panic","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc4","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I've been playing around with GHC 8.0.1-rc4 release and got a panic from the following (stripped down) code:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeInType #-}\r\n\r\ndata Nat = Z | S Nat\r\n\r\nclass C (n :: Nat) where\r\n type T n :: Nat\r\n f :: (a :: T n)\r\n}}}\r\n\r\n{{{\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.0.0.20160421 for x86_64-apple-darwin):\r\n\tisInjectiveTyCon sees a TcTyCon T\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12045Visible kind application2019-07-07T18:27:52ZIcelandjackVisible kind applicationI've wanted this for a while
```
ghci> :kind (:~:)
(:~:) :: k -> k -> Type
```
```
ghci> :kind (:~:) @(Type -> Type)
(:~:) @(Type -> Type) :: (Type -> Type) -> (Type -> Type) -> Type
ghci> :kind (:~:) @(Type -> Type) []
(:~:) @(Type -> Type) [] :: (Type -> Type) -> Type
ghci> :kind (:~:) @(Type -> Type) [] Maybe
(:~:) @(Type -> Type) [] Maybe :: Type
```
Working like
```
ghci> type Same k (a::k) (b::k) = a :~: b
ghci> :kind Same
Same :: forall k -> k -> k -> *
```
```
ghci> :kind Same (Type -> Type)
Same (Type -> Type) :: (Type -> Type) -> (Type -> Type) -> *
ghci> :kind Same (Type -> Type) []
Same (Type -> Type) [] :: (Type -> Type) -> *
ghci> :kind Same (Type -> Type) [] Maybe
Same (Type -> Type) [] Maybe :: *
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 8.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":"Visible kind application","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeApplications","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"I've wanted this for a while\r\n\r\n{{{\r\nghci> :kind (:~:)\r\n(:~:) :: k -> k -> Type\r\n}}}\r\n\r\n{{{\r\nghci> :kind (:~:) @(Type -> Type)\r\n(:~:) @(Type -> Type) :: (Type -> Type) -> (Type -> Type) -> Type\r\n\r\nghci> :kind (:~:) @(Type -> Type) []\r\n(:~:) @(Type -> Type) [] :: (Type -> Type) -> Type\r\n\r\nghci> :kind (:~:) @(Type -> Type) [] Maybe\r\n(:~:) @(Type -> Type) [] Maybe :: Type\r\n}}}\r\n\r\nWorking like\r\n\r\n{{{\r\nghci> type Same k (a::k) (b::k) = a :~: b\r\nghci> :kind Same\r\nSame :: forall k -> k -> k -> *\r\n}}}\r\n\r\n{{{\r\nghci> :kind Same (Type -> Type)\r\nSame (Type -> Type) :: (Type -> Type) -> (Type -> Type) -> *\r\nghci> :kind Same (Type -> Type) []\r\nSame (Type -> Type) [] :: (Type -> Type) -> *\r\nghci> :kind Same (Type -> Type) [] Maybe\r\nSame (Type -> Type) [] Maybe :: *\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->I've wanted this for a while
```
ghci> :kind (:~:)
(:~:) :: k -> k -> Type
```
```
ghci> :kind (:~:) @(Type -> Type)
(:~:) @(Type -> Type) :: (Type -> Type) -> (Type -> Type) -> Type
ghci> :kind (:~:) @(Type -> Type) []
(:~:) @(Type -> Type) [] :: (Type -> Type) -> Type
ghci> :kind (:~:) @(Type -> Type) [] Maybe
(:~:) @(Type -> Type) [] Maybe :: Type
```
Working like
```
ghci> type Same k (a::k) (b::k) = a :~: b
ghci> :kind Same
Same :: forall k -> k -> k -> *
```
```
ghci> :kind Same (Type -> Type)
Same (Type -> Type) :: (Type -> Type) -> (Type -> Type) -> *
ghci> :kind Same (Type -> Type) []
Same (Type -> Type) [] :: (Type -> Type) -> *
ghci> :kind Same (Type -> Type) [] Maybe
Same (Type -> Type) [] Maybe :: *
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 8.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":"Visible kind application","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeApplications","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"I've wanted this for a while\r\n\r\n{{{\r\nghci> :kind (:~:)\r\n(:~:) :: k -> k -> Type\r\n}}}\r\n\r\n{{{\r\nghci> :kind (:~:) @(Type -> Type)\r\n(:~:) @(Type -> Type) :: (Type -> Type) -> (Type -> Type) -> Type\r\n\r\nghci> :kind (:~:) @(Type -> Type) []\r\n(:~:) @(Type -> Type) [] :: (Type -> Type) -> Type\r\n\r\nghci> :kind (:~:) @(Type -> Type) [] Maybe\r\n(:~:) @(Type -> Type) [] Maybe :: Type\r\n}}}\r\n\r\nWorking like\r\n\r\n{{{\r\nghci> type Same k (a::k) (b::k) = a :~: b\r\nghci> :kind Same\r\nSame :: forall k -> k -> k -> *\r\n}}}\r\n\r\n{{{\r\nghci> :kind Same (Type -> Type)\r\nSame (Type -> Type) :: (Type -> Type) -> (Type -> Type) -> *\r\nghci> :kind Same (Type -> Type) []\r\nSame (Type -> Type) [] :: (Type -> Type) -> *\r\nghci> :kind Same (Type -> Type) [] Maybe\r\nSame (Type -> Type) [] Maybe :: *\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1My NguyenMy Nguyenhttps://gitlab.haskell.org/ghc/ghc/-/issues/12030GHCi Proposal: Display (Data.Kind.)Type instead of *2019-07-07T18:27:55ZIcelandjackGHCi Proposal: Display (Data.Kind.)Type instead of *This is premature but what the darn,
```
>>> :kind Maybe
Maybe :: Type -> Type
>>> :kind StateT
StateT :: Type -> (Type -> Type) -> Type -> Type
>>> :kind Eq
Eq :: Type -> Constraint
>>> :info Functor
class Functor (f :: Type -> Type) where
...
```
`*` throws students off in my experience, makes it seem scarier than it is. Symbols are harder to search for and understand without documentation, `Type` on the other hand is descriptive.
There are arguments against:
1. It's a recent feature that is subject to change.
1. `*` is established in questions online, educational material, logs and blogs.
1. `Type` is not in scope by default: user cannot query GHCi.
`*` is established and searching for “Haskell asterisk” yields a lot resources but [‘\*’ is also a wildcard](https://support.google.com/websearch/answer/2466433?hl=en) in Google and ignored by GitHub. With time `Type` would be a good search term but currently it's chicken-and-the-egg.
Previous versions of GHCi error on `:kind *` and `:info *` only shows multiplication so that wouldn't be a huge difference but we can qualify by default:
```
>>> :kind Maybe
Maybe :: Data.Kind.Type -> Data.Kind.Type
>>> :kind StateT
StateT :: Data.Kind.Type -> (Data.Kind.Type -> Data.Kind.Type) -> Data.Kind.Type -> Data.Kind.Type
>>> :kind Eq
Eq :: Data.Kind.Type -> Constraint
>>> :info Functor
class Functor (f :: Data.Kind.Type -> Data.Kind.Type) where
...
```
or display `*` normally and only when `TypeInType` is set do we display `Type`. I don't love it (and love `GHC.Types.Type` slightly less) but there is a precedent for unqualified names, browsing the Prelude for example:
```hs
($) ::
forall (r :: GHC.Types.RuntimeRep) a (b :: TYPE r).
(a -> b) -> a -> b
undefined ::
forall (r :: GHC.Types.RuntimeRep) (a :: TYPE r).
GHC.Stack.Types.HasCallStack =>
a
```
__If__ the consensus is that this will happen sometime down the line consider that each passing release means many more books and blog posts get written using `*`.
I wasn't planning on resulting to scare tactics but [here we are](https://www.peoria.com/spaw/spawimages/members/member60763/shoot_this_dog.jpg)...
----
If needed a migration plan can be drafted like the Semigroup/FTP/AMP/BBP/MonadFail/expanding Float/... proposals, possibly culminating in `Type` fully replacing `*` and being imported by default. I'm sure there are some further reaching consequences to this and better arguments against.This is premature but what the darn,
```
>>> :kind Maybe
Maybe :: Type -> Type
>>> :kind StateT
StateT :: Type -> (Type -> Type) -> Type -> Type
>>> :kind Eq
Eq :: Type -> Constraint
>>> :info Functor
class Functor (f :: Type -> Type) where
...
```
`*` throws students off in my experience, makes it seem scarier than it is. Symbols are harder to search for and understand without documentation, `Type` on the other hand is descriptive.
There are arguments against:
1. It's a recent feature that is subject to change.
1. `*` is established in questions online, educational material, logs and blogs.
1. `Type` is not in scope by default: user cannot query GHCi.
`*` is established and searching for “Haskell asterisk” yields a lot resources but [‘\*’ is also a wildcard](https://support.google.com/websearch/answer/2466433?hl=en) in Google and ignored by GitHub. With time `Type` would be a good search term but currently it's chicken-and-the-egg.
Previous versions of GHCi error on `:kind *` and `:info *` only shows multiplication so that wouldn't be a huge difference but we can qualify by default:
```
>>> :kind Maybe
Maybe :: Data.Kind.Type -> Data.Kind.Type
>>> :kind StateT
StateT :: Data.Kind.Type -> (Data.Kind.Type -> Data.Kind.Type) -> Data.Kind.Type -> Data.Kind.Type
>>> :kind Eq
Eq :: Data.Kind.Type -> Constraint
>>> :info Functor
class Functor (f :: Data.Kind.Type -> Data.Kind.Type) where
...
```
or display `*` normally and only when `TypeInType` is set do we display `Type`. I don't love it (and love `GHC.Types.Type` slightly less) but there is a precedent for unqualified names, browsing the Prelude for example:
```hs
($) ::
forall (r :: GHC.Types.RuntimeRep) a (b :: TYPE r).
(a -> b) -> a -> b
undefined ::
forall (r :: GHC.Types.RuntimeRep) (a :: TYPE r).
GHC.Stack.Types.HasCallStack =>
a
```
__If__ the consensus is that this will happen sometime down the line consider that each passing release means many more books and blog posts get written using `*`.
I wasn't planning on resulting to scare tactics but [here we are](https://www.peoria.com/spaw/spawimages/members/member60763/shoot_this_dog.jpg)...
----
If needed a migration plan can be drafted like the Semigroup/FTP/AMP/BBP/MonadFail/expanding Float/... proposals, possibly culminating in `Type` fully replacing `*` and being imported by default. I'm sure there are some further reaching consequences to this and better arguments against.8.6.1johnleojohnleohttps://gitlab.haskell.org/ghc/ghc/-/issues/12029Notify user to import * from Data.Kind with TypeInType on2019-07-07T18:27:55ZIcelandjackNotify user to import * from Data.Kind with TypeInType onWith `TypeInType` asking for the kind of `*` gives the user a warning to import it
```
ghci> :set -XTypeInType
ghci> :k *
<interactive>:1:1: error:
Not in scope: type constructor or class ‘*’
NB: With TypeInType, you must import * from Data.Kind
<interactive>:1:1: error:
Illegal operator ‘*’ in type ‘*’
Use TypeOperators to allow operators in types
<interactive>:1:1: error: Operator applied to too few arguments: *
```
Should a similar warning be issued when she asks for information on it
```
ghci> :i *
class Num a where
...
(*) :: a -> a -> a
...
-- Defined in ‘GHC.Num’
infixl 7 *
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 8.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | lowest |
| Resolution | Unresolved |
| Component | GHCi |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Notify user to import * from Data.Kind with TypeInType on","status":"New","operating_system":"","component":"GHCi","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"With `TypeInType` asking for the kind of `*` gives the user a warning to import it\r\n\r\n{{{\r\nghci> :set -XTypeInType \r\nghci> :k *\r\n\r\n<interactive>:1:1: error:\r\n Not in scope: type constructor or class ‘*’\r\n NB: With TypeInType, you must import * from Data.Kind\r\n\r\n<interactive>:1:1: error:\r\n Illegal operator ‘*’ in type ‘*’\r\n Use TypeOperators to allow operators in types\r\n\r\n<interactive>:1:1: error: Operator applied to too few arguments: *\r\n}}}\r\n\r\nShould a similar warning be issued when she asks for information on it\r\n\r\n{{{\r\nghci> :i *\r\nclass Num a where\r\n ...\r\n (*) :: a -> a -> a\r\n ...\r\n -- Defined in ‘GHC.Num’\r\ninfixl 7 *\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->With `TypeInType` asking for the kind of `*` gives the user a warning to import it
```
ghci> :set -XTypeInType
ghci> :k *
<interactive>:1:1: error:
Not in scope: type constructor or class ‘*’
NB: With TypeInType, you must import * from Data.Kind
<interactive>:1:1: error:
Illegal operator ‘*’ in type ‘*’
Use TypeOperators to allow operators in types
<interactive>:1:1: error: Operator applied to too few arguments: *
```
Should a similar warning be issued when she asks for information on it
```
ghci> :i *
class Num a where
...
(*) :: a -> a -> a
...
-- Defined in ‘GHC.Num’
infixl 7 *
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 8.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | lowest |
| Resolution | Unresolved |
| Component | GHCi |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Notify user to import * from Data.Kind with TypeInType on","status":"New","operating_system":"","component":"GHCi","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"With `TypeInType` asking for the kind of `*` gives the user a warning to import it\r\n\r\n{{{\r\nghci> :set -XTypeInType \r\nghci> :k *\r\n\r\n<interactive>:1:1: error:\r\n Not in scope: type constructor or class ‘*’\r\n NB: With TypeInType, you must import * from Data.Kind\r\n\r\n<interactive>:1:1: error:\r\n Illegal operator ‘*’ in type ‘*’\r\n Use TypeOperators to allow operators in types\r\n\r\n<interactive>:1:1: error: Operator applied to too few arguments: *\r\n}}}\r\n\r\nShould a similar warning be issued when she asks for information on it\r\n\r\n{{{\r\nghci> :i *\r\nclass Num a where\r\n ...\r\n (*) :: a -> a -> a\r\n ...\r\n -- Defined in ‘GHC.Num’\r\ninfixl 7 *\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->johnleojohnleohttps://gitlab.haskell.org/ghc/ghc/-/issues/11995Can't infer type2019-07-07T18:28:05ZIcelandjackCan't infer type```hs
{-# LANGUAGE RankNTypes, LambdaCase, TypeOperators,
TypeInType, UnicodeSyntax, GADTs #-}
module T11995 where
import Data.Kind
data NP :: forall k. (ĸ → Type) → ([k] → Type) where
Nil :: NP f '[]
(:*) :: f x → NP f xs → NP f (x:xs)
newtype K a b = K a deriving Show
unK (K a) = a
h'collapse :: NP (K a) xs -> [a]
h'collapse = \case
Nil -> []
K x:*xs -> x : h'collapse xs
```
if we replace `xs` by an underscore:
```
tJN0.hs:13:29-30: error: …
• Could not deduce: (xs :: [ĸ]) ~~ ((':) ĸ x xs :: [ĸ])
from the context: ((k :: *) ~~ (ĸ :: *),
(t :: [k]) ~~ ((':) ĸ x xs :: [ĸ]))
bound by a pattern with constructor:
:* :: forall k (f :: k -> *) (x :: k) (xs :: [k]).
f x -> NP k k f xs -> NP k k f ((':) k x xs),
in a case alternative
at /tmp/tJN0.hs:13:3-9
‘xs’ is a rigid type variable bound by
a pattern with constructor:
:* :: forall k (f :: k -> *) (x :: k) (xs :: [k]).
f x -> NP k k f xs -> NP k k f ((':) k x xs),
in a case alternative
at /tmp/tJN0.hs:13:3
Expected type: NP ĸ k (K ĸ a) t
Actual type: NP ĸ ĸ (K ĸ a) xs
• In the first argument of ‘h'collapse’, namely ‘xs’
In the second argument of ‘(:)’, namely ‘h'collapse xs’
In the expression: x : h'collapse xs
• Relevant bindings include
xs :: NP ĸ ĸ (K ĸ a) xs (bound at /tmp/tJN0.hs:13:8)
h'collapse :: NP ĸ k (K ĸ a) t -> [a] (bound at /tmp/tJN0.hs:11:1)
Compilation failed.
```
Should it not be able to infer that?
The Glorious Glasgow Haskell Compilation System, version 8.1.20160419```hs
{-# LANGUAGE RankNTypes, LambdaCase, TypeOperators,
TypeInType, UnicodeSyntax, GADTs #-}
module T11995 where
import Data.Kind
data NP :: forall k. (ĸ → Type) → ([k] → Type) where
Nil :: NP f '[]
(:*) :: f x → NP f xs → NP f (x:xs)
newtype K a b = K a deriving Show
unK (K a) = a
h'collapse :: NP (K a) xs -> [a]
h'collapse = \case
Nil -> []
K x:*xs -> x : h'collapse xs
```
if we replace `xs` by an underscore:
```
tJN0.hs:13:29-30: error: …
• Could not deduce: (xs :: [ĸ]) ~~ ((':) ĸ x xs :: [ĸ])
from the context: ((k :: *) ~~ (ĸ :: *),
(t :: [k]) ~~ ((':) ĸ x xs :: [ĸ]))
bound by a pattern with constructor:
:* :: forall k (f :: k -> *) (x :: k) (xs :: [k]).
f x -> NP k k f xs -> NP k k f ((':) k x xs),
in a case alternative
at /tmp/tJN0.hs:13:3-9
‘xs’ is a rigid type variable bound by
a pattern with constructor:
:* :: forall k (f :: k -> *) (x :: k) (xs :: [k]).
f x -> NP k k f xs -> NP k k f ((':) k x xs),
in a case alternative
at /tmp/tJN0.hs:13:3
Expected type: NP ĸ k (K ĸ a) t
Actual type: NP ĸ ĸ (K ĸ a) xs
• In the first argument of ‘h'collapse’, namely ‘xs’
In the second argument of ‘(:)’, namely ‘h'collapse xs’
In the expression: x : h'collapse xs
• Relevant bindings include
xs :: NP ĸ ĸ (K ĸ a) xs (bound at /tmp/tJN0.hs:13:8)
h'collapse :: NP ĸ k (K ĸ a) t -> [a] (bound at /tmp/tJN0.hs:11:1)
Compilation failed.
```
Should it not be able to infer that?
The Glorious Glasgow Haskell Compilation System, version 8.1.201604198.2.2https://gitlab.haskell.org/ghc/ghc/-/issues/11966Surprising behavior with higher-rank quantification of kind variables2019-07-07T18:28:13ZOllie CharlesSurprising behavior with higher-rank quantification of kind variablesSorry about the rubbish title. I wrote the following code, which type checks:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Test where
import Data.Kind (Type)
-- Simplification
type family Col (f :: k -> j) (x :: k) :: Type
-- Base types
data PGBaseType = PGInteger | PGText
-- Transformations
data Column t = Column Symbol t
newtype Nullable t = Nullable t
newtype HasDefault t = HasDefault t
-- Interpretations
data Expr k
data Record (f :: forall k. k -> Type) =
Record {rX :: Col f ('Column "x" 'PGInteger)
,rY :: Col f ('Column "y" ('Nullable 'PGInteger))
,rZ :: Col f ('HasDefault 'PGText)}
```
However, if I play with this in GHCI, I can get the following error:
```
λ> let x = undefined :: Record Expr
<interactive>:136:29-32: error:
• Expected kind ‘forall k. k -> Type’,
but ‘Expr’ has kind ‘forall k. k -> *’
• In the first argument of ‘Record’, namely ‘Expr’
In an expression type signature: Record Expr
In the expression: undefined :: Record Expr
```
It seems that if I write
```hs
data Expr :: forall k. k -> Type
```
things work, but I'm unclear if/why that is necessary, and the error message certainly needs to be fixed.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1-rc3 |
| 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":"Surprising behavior with higher-rank quantification of kind variables","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Sorry about the rubbish title. I wrote the following code, which type checks:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n\r\nmodule Test where\r\n\r\nimport Data.Kind (Type)\r\n\r\n-- Simplification\r\ntype family Col (f :: k -> j) (x :: k) :: Type\r\n\r\n-- Base types\r\ndata PGBaseType = PGInteger | PGText\r\n\r\n-- Transformations\r\ndata Column t = Column Symbol t\r\nnewtype Nullable t = Nullable t\r\nnewtype HasDefault t = HasDefault t\r\n\r\n-- Interpretations\r\ndata Expr k\r\n\r\ndata Record (f :: forall k. k -> Type) =\r\n Record {rX :: Col f ('Column \"x\" 'PGInteger)\r\n ,rY :: Col f ('Column \"y\" ('Nullable 'PGInteger))\r\n ,rZ :: Col f ('HasDefault 'PGText)}\r\n\r\n}}}\r\n\r\nHowever, if I play with this in GHCI, I can get the following error:\r\n\r\n{{{\r\nλ> let x = undefined :: Record Expr\r\n\r\n<interactive>:136:29-32: error:\r\n • Expected kind ‘forall k. k -> Type’,\r\n but ‘Expr’ has kind ‘forall k. k -> *’\r\n • In the first argument of ‘Record’, namely ‘Expr’\r\n In an expression type signature: Record Expr\r\n In the expression: undefined :: Record Expr\r\n}}}\r\n\r\nIt seems that if I write\r\n\r\n{{{#!hs\r\ndata Expr :: forall k. k -> Type\r\n}}}\r\n\r\nthings work, but I'm unclear if/why that is necessary, and the error message certainly needs to be fixed.","type_of_failure":"OtherFailure","blocking":[]} -->Sorry about the rubbish title. I wrote the following code, which type checks:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Test where
import Data.Kind (Type)
-- Simplification
type family Col (f :: k -> j) (x :: k) :: Type
-- Base types
data PGBaseType = PGInteger | PGText
-- Transformations
data Column t = Column Symbol t
newtype Nullable t = Nullable t
newtype HasDefault t = HasDefault t
-- Interpretations
data Expr k
data Record (f :: forall k. k -> Type) =
Record {rX :: Col f ('Column "x" 'PGInteger)
,rY :: Col f ('Column "y" ('Nullable 'PGInteger))
,rZ :: Col f ('HasDefault 'PGText)}
```
However, if I play with this in GHCI, I can get the following error:
```
λ> let x = undefined :: Record Expr
<interactive>:136:29-32: error:
• Expected kind ‘forall k. k -> Type’,
but ‘Expr’ has kind ‘forall k. k -> *’
• In the first argument of ‘Record’, namely ‘Expr’
In an expression type signature: Record Expr
In the expression: undefined :: Record Expr
```
It seems that if I write
```hs
data Expr :: forall k. k -> Type
```
things work, but I'm unclear if/why that is necessary, and the error message certainly needs to be fixed.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1-rc3 |
| 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":"Surprising behavior with higher-rank quantification of kind variables","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Sorry about the rubbish title. I wrote the following code, which type checks:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n\r\nmodule Test where\r\n\r\nimport Data.Kind (Type)\r\n\r\n-- Simplification\r\ntype family Col (f :: k -> j) (x :: k) :: Type\r\n\r\n-- Base types\r\ndata PGBaseType = PGInteger | PGText\r\n\r\n-- Transformations\r\ndata Column t = Column Symbol t\r\nnewtype Nullable t = Nullable t\r\nnewtype HasDefault t = HasDefault t\r\n\r\n-- Interpretations\r\ndata Expr k\r\n\r\ndata Record (f :: forall k. k -> Type) =\r\n Record {rX :: Col f ('Column \"x\" 'PGInteger)\r\n ,rY :: Col f ('Column \"y\" ('Nullable 'PGInteger))\r\n ,rZ :: Col f ('HasDefault 'PGText)}\r\n\r\n}}}\r\n\r\nHowever, if I play with this in GHCI, I can get the following error:\r\n\r\n{{{\r\nλ> let x = undefined :: Record Expr\r\n\r\n<interactive>:136:29-32: error:\r\n • Expected kind ‘forall k. k -> Type’,\r\n but ‘Expr’ has kind ‘forall k. k -> *’\r\n • In the first argument of ‘Record’, namely ‘Expr’\r\n In an expression type signature: Record Expr\r\n In the expression: undefined :: Record Expr\r\n}}}\r\n\r\nIt seems that if I write\r\n\r\n{{{#!hs\r\ndata Expr :: forall k. k -> Type\r\n}}}\r\n\r\nthings work, but I'm unclear if/why that is necessary, and the error message certainly needs to be fixed.","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/11964Without TypeInType, inconsistently accepts Data.Kind.Type but not type synonym2019-07-07T18:28:14ZEdward Z. YangWithout TypeInType, inconsistently accepts Data.Kind.Type but not type synonymFor convenience, I'll use GHCi to demonstrate flag behavior. First, we define a file:
```
{-# LANGUAGE TypeInType #-}
import Data.Kind
type Star = Type
newtype T k (t :: k) = T ()
```
Next, we load it up in GHCi, WITHOUT `-XTypeInType`. Now we observe strange behavior:
```
ezyang@sabre:~$ ghc-8.0 --interactive C.hs
GHCi, version 8.0.0.20160204: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( C.hs, interpreted )
Ok, modules loaded: Main.
*Main> :k T Type Int
T Type Int :: *
*Main> :k T Star Int
<interactive>:1:3: error:
• Data constructor ‘Star’ cannot be used here
(Perhaps you intended to use DataKinds)
• In the first argument of ‘T’, namely ‘Star’
In the type ‘T Star Int’
```
Of course, if we pass `-TypeInType` to GHCi that fixes the problem (BTW, `DataKinds` does NOT solve the problem.)For convenience, I'll use GHCi to demonstrate flag behavior. First, we define a file:
```
{-# LANGUAGE TypeInType #-}
import Data.Kind
type Star = Type
newtype T k (t :: k) = T ()
```
Next, we load it up in GHCi, WITHOUT `-XTypeInType`. Now we observe strange behavior:
```
ezyang@sabre:~$ ghc-8.0 --interactive C.hs
GHCi, version 8.0.0.20160204: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( C.hs, interpreted )
Ok, modules loaded: Main.
*Main> :k T Type Int
T Type Int :: *
*Main> :k T Star Int
<interactive>:1:3: error:
• Data constructor ‘Star’ cannot be used here
(Perhaps you intended to use DataKinds)
• In the first argument of ‘T’, namely ‘Star’
In the type ‘T Star Int’
```
Of course, if we pass `-TypeInType` to GHCi that fixes the problem (BTW, `DataKinds` does NOT solve the problem.)Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11963GHC introduces kind equality without TypeInType2019-07-07T18:28:14ZEdward Z. YangGHC introduces kind equality without TypeInTypeThe following program is accepted by GHC 8.0 rc2
```
{-# LANGUAGE GADTs, PolyKinds, RankNTypes #-}
data Typ k t where
Typ :: (forall (a :: k -> *). a t -> a t) -> Typ k t
```
This probably shouldn't be accepted, because this is a circuitous way of saying:
```
{-# LANGUAGE TypeInType #-}
data Typ k (t :: k) = Typ
```
which does not work without `TypeInType`. Or perhaps both should be accepted without `TypeInType`?
Printing with explicit kinds makes it clear why the obvious check didn't fire:
```
ezyang@sabre:~$ ghc-8.0 --interactive B.hs -fprint-explicit-kinds
GHCi, version 8.0.0.20160204: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( B.hs, interpreted )
Ok, modules loaded: Main.
*Main> :info Typ
type role Typ nominal nominal nominal
data Typ k k1 (t :: k) where
Typ :: forall k (t :: k).
(forall (a :: k -> *). a t -> a t) -> Typ k k t
-- Defined at B.hs:2:1
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1-rc2 |
| 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":"GHC introduces kind equality without TypeInType","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.0.1-rc2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program is accepted by GHC 8.0 rc2\r\n\r\n{{{\r\n{-# LANGUAGE GADTs, PolyKinds, RankNTypes #-}\r\ndata Typ k t where\r\n Typ :: (forall (a :: k -> *). a t -> a t) -> Typ k t\r\n}}}\r\n\r\nThis probably shouldn't be accepted, because this is a circuitous way of saying:\r\n\r\n{{{\r\n{-# LANGUAGE TypeInType #-}\r\ndata Typ k (t :: k) = Typ\r\n}}}\r\n\r\nwhich does not work without `TypeInType`. Or perhaps both should be accepted without `TypeInType`?\r\n\r\nPrinting with explicit kinds makes it clear why the obvious check didn't fire:\r\n\r\n{{{\r\nezyang@sabre:~$ ghc-8.0 --interactive B.hs -fprint-explicit-kinds\r\nGHCi, version 8.0.0.20160204: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( B.hs, interpreted )\r\nOk, modules loaded: Main.\r\n*Main> :info Typ\r\ntype role Typ nominal nominal nominal\r\ndata Typ k k1 (t :: k) where\r\n Typ :: forall k (t :: k).\r\n (forall (a :: k -> *). a t -> a t) -> Typ k k t\r\n \t-- Defined at B.hs:2:1\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->The following program is accepted by GHC 8.0 rc2
```
{-# LANGUAGE GADTs, PolyKinds, RankNTypes #-}
data Typ k t where
Typ :: (forall (a :: k -> *). a t -> a t) -> Typ k t
```
This probably shouldn't be accepted, because this is a circuitous way of saying:
```
{-# LANGUAGE TypeInType #-}
data Typ k (t :: k) = Typ
```
which does not work without `TypeInType`. Or perhaps both should be accepted without `TypeInType`?
Printing with explicit kinds makes it clear why the obvious check didn't fire:
```
ezyang@sabre:~$ ghc-8.0 --interactive B.hs -fprint-explicit-kinds
GHCi, version 8.0.0.20160204: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( B.hs, interpreted )
Ok, modules loaded: Main.
*Main> :info Typ
type role Typ nominal nominal nominal
data Typ k k1 (t :: k) where
Typ :: forall k (t :: k).
(forall (a :: k -> *). a t -> a t) -> Typ k k t
-- Defined at B.hs:2:1
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1-rc2 |
| 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":"GHC introduces kind equality without TypeInType","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.0.1-rc2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program is accepted by GHC 8.0 rc2\r\n\r\n{{{\r\n{-# LANGUAGE GADTs, PolyKinds, RankNTypes #-}\r\ndata Typ k t where\r\n Typ :: (forall (a :: k -> *). a t -> a t) -> Typ k t\r\n}}}\r\n\r\nThis probably shouldn't be accepted, because this is a circuitous way of saying:\r\n\r\n{{{\r\n{-# LANGUAGE TypeInType #-}\r\ndata Typ k (t :: k) = Typ\r\n}}}\r\n\r\nwhich does not work without `TypeInType`. Or perhaps both should be accepted without `TypeInType`?\r\n\r\nPrinting with explicit kinds makes it clear why the obvious check didn't fire:\r\n\r\n{{{\r\nezyang@sabre:~$ ghc-8.0 --interactive B.hs -fprint-explicit-kinds\r\nGHCi, version 8.0.0.20160204: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( B.hs, interpreted )\r\nOk, modules loaded: Main.\r\n*Main> :info Typ\r\ntype role Typ nominal nominal nominal\r\ndata Typ k k1 (t :: k) where\r\n Typ :: forall k (t :: k).\r\n (forall (a :: k -> *). a t -> a t) -> Typ k k t\r\n \t-- Defined at B.hs:2:1\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1johnleojohnleohttps://gitlab.haskell.org/ghc/ghc/-/issues/11962Support induction recursion2020-01-06T11:26:23ZRichard Eisenbergrae@richarde.devSupport induction recursionNow that we have `-XTypeInType`, let's take it a step further and allow induction recursion. This feature exists in Agda and Idris. Here is a short example of what can be done in Agda:
```
mutual
-- Codes for types.
data U : Set where
nat : U
pi : (a : U) → (El a → U) → U
-- A function that interprets codes as actual types.
El : U → Set
El nat = ℕ
El (pi a b) = (x : El a) → El (b x)
```
Note that the `U` datatype and the `El` function depend on each other. But if you look more closely, the header for `U` does not depend on `El`; only the constructors of `U` depend on `El`. So if we typecheck `U : Set` first, then `El : U → Set`, then the constructors of `U`, then the equations of `El`, we're OK.
Translation into Haskell:
```
import Data.Kind
data family Sing (a :: k) -- we still require singletons
data U :: Type where
Nat :: U
Pi :: Sing (a :: U) -> (El a -> U) -> U
type family El (u :: U) :: Type where
El 'Nat = Int
El (Pi a b) = forall (x :: El a). Sing x -> El (b x)
```
This currently errors with
```
• Type constructor ‘U’ cannot be used here
(it is defined and used in the same recursive group)
• In the kind ‘U’
```
It needn't error. (I'm cheating a bit here, because for unrelated reasons, we can't return a `forall` on the right-hand side of a type family. But that's not the issue at hand.)
I have some very sketchy notes on how we might do this [here](https://gitlab.haskell.org/ghc/ghc/wikis/dependent-haskell/internal#separating-type-signatures-from-definitions).
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 8.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":"Support induction recursion","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Now that we have `-XTypeInType`, let's take it a step further and allow induction recursion. This feature exists in Agda and Idris. Here is a short example of what can be done in Agda:\r\n\r\n{{{\r\n mutual\r\n -- Codes for types.\r\n\r\n data U : Set where\r\n nat : U\r\n pi : (a : U) → (El a → U) → U\r\n\r\n -- A function that interprets codes as actual types.\r\n\r\n El : U → Set\r\n El nat = ℕ\r\n El (pi a b) = (x : El a) → El (b x)\r\n}}}\r\n\r\nNote that the `U` datatype and the `El` function depend on each other. But if you look more closely, the header for `U` does not depend on `El`; only the constructors of `U` depend on `El`. So if we typecheck `U : Set` first, then `El : U → Set`, then the constructors of `U`, then the equations of `El`, we're OK.\r\n\r\nTranslation into Haskell:\r\n\r\n{{{\r\nimport Data.Kind\r\n\r\ndata family Sing (a :: k) -- we still require singletons\r\n\r\ndata U :: Type where\r\n Nat :: U\r\n Pi :: Sing (a :: U) -> (El a -> U) -> U\r\n\r\ntype family El (u :: U) :: Type where\r\n El 'Nat = Int\r\n El (Pi a b) = forall (x :: El a). Sing x -> El (b x)\r\n}}}\r\n\r\nThis currently errors with\r\n\r\n{{{\r\n • Type constructor ‘U’ cannot be used here\r\n (it is defined and used in the same recursive group)\r\n • In the kind ‘U’\r\n}}}\r\n\r\nIt needn't error. (I'm cheating a bit here, because for unrelated reasons, we can't return a `forall` on the right-hand side of a type family. But that's not the issue at hand.)\r\n\r\nI have some very sketchy notes on how we might do this [wiki:DependentHaskell/Internal#Separatingtypesignaturesfromdefinitions here].","type_of_failure":"OtherFailure","blocking":[]} -->Now that we have `-XTypeInType`, let's take it a step further and allow induction recursion. This feature exists in Agda and Idris. Here is a short example of what can be done in Agda:
```
mutual
-- Codes for types.
data U : Set where
nat : U
pi : (a : U) → (El a → U) → U
-- A function that interprets codes as actual types.
El : U → Set
El nat = ℕ
El (pi a b) = (x : El a) → El (b x)
```
Note that the `U` datatype and the `El` function depend on each other. But if you look more closely, the header for `U` does not depend on `El`; only the constructors of `U` depend on `El`. So if we typecheck `U : Set` first, then `El : U → Set`, then the constructors of `U`, then the equations of `El`, we're OK.
Translation into Haskell:
```
import Data.Kind
data family Sing (a :: k) -- we still require singletons
data U :: Type where
Nat :: U
Pi :: Sing (a :: U) -> (El a -> U) -> U
type family El (u :: U) :: Type where
El 'Nat = Int
El (Pi a b) = forall (x :: El a). Sing x -> El (b x)
```
This currently errors with
```
• Type constructor ‘U’ cannot be used here
(it is defined and used in the same recursive group)
• In the kind ‘U’
```
It needn't error. (I'm cheating a bit here, because for unrelated reasons, we can't return a `forall` on the right-hand side of a type family. But that's not the issue at hand.)
I have some very sketchy notes on how we might do this [here](https://gitlab.haskell.org/ghc/ghc/wikis/dependent-haskell/internal#separating-type-signatures-from-definitions).
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 8.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":"Support induction recursion","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Now that we have `-XTypeInType`, let's take it a step further and allow induction recursion. This feature exists in Agda and Idris. Here is a short example of what can be done in Agda:\r\n\r\n{{{\r\n mutual\r\n -- Codes for types.\r\n\r\n data U : Set where\r\n nat : U\r\n pi : (a : U) → (El a → U) → U\r\n\r\n -- A function that interprets codes as actual types.\r\n\r\n El : U → Set\r\n El nat = ℕ\r\n El (pi a b) = (x : El a) → El (b x)\r\n}}}\r\n\r\nNote that the `U` datatype and the `El` function depend on each other. But if you look more closely, the header for `U` does not depend on `El`; only the constructors of `U` depend on `El`. So if we typecheck `U : Set` first, then `El : U → Set`, then the constructors of `U`, then the equations of `El`, we're OK.\r\n\r\nTranslation into Haskell:\r\n\r\n{{{\r\nimport Data.Kind\r\n\r\ndata family Sing (a :: k) -- we still require singletons\r\n\r\ndata U :: Type where\r\n Nat :: U\r\n Pi :: Sing (a :: U) -> (El a -> U) -> U\r\n\r\ntype family El (u :: U) :: Type where\r\n El 'Nat = Int\r\n El (Pi a b) = forall (x :: El a). Sing x -> El (b x)\r\n}}}\r\n\r\nThis currently errors with\r\n\r\n{{{\r\n • Type constructor ‘U’ cannot be used here\r\n (it is defined and used in the same recursive group)\r\n • In the kind ‘U’\r\n}}}\r\n\r\nIt needn't error. (I'm cheating a bit here, because for unrelated reasons, we can't return a `forall` on the right-hand side of a type family. But that's not the issue at hand.)\r\n\r\nI have some very sketchy notes on how we might do this [wiki:DependentHaskell/Internal#Separatingtypesignaturesfromdefinitions here].","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11821Internal error: not in scope during type checking, but it passed the renamer2019-07-07T18:28:23ZdarchonInternal error: not in scope during type checking, but it passed the renamerWhile trying to get the singletons package to compile on GHC8 (https://github.com/goldfirere/singletons/pull/142), I encountered the following error while trying to track down a bug:
```
[1 of 1] Compiling NotInScope ( NotInScope.hs, interpreted )
NotInScope.hs:22:20: error:
• GHC internal error: ‘b’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: [a1lm :-> Type variable ‘b’ = b,
a1lA :-> Type variable ‘l1’ = l1, a1lB :-> Type variable ‘l2’ = l2,
a1lC :-> Type variable ‘l3’ = l3, a1lE :-> Type variable ‘a’ = a,
a1lF :-> Type variable ‘l4’ = l4, r1aq :-> ATcTyCon Lgo,
r1aG :-> ATcTyCon Lgo1, r1aI :-> ATcTyCon Lgo2]
• In the kind ‘b’
In the definition of data constructor ‘Lgo1KindInference’
In the data declaration for ‘Lgo1’
```
for the following code:
```
{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, UndecidableInstances #-}
module NotInScope where
import Data.Proxy
type KindOf (a :: k) = ('KProxy :: KProxy k)
data TyFun :: * -> * -> *
type family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2
data Lgo2 l1
l2
l3
(l4 :: b)
(l5 :: TyFun [a] b)
= forall (arg :: [a]) . KindOf (Apply (Lgo2 l1 l2 l3 l4) arg) ~ KindOf (Lgo l1 l2 l3 l4 arg) =>
Lgo2KindInference
data Lgo1 l1
l2
l3
(l4 :: TyFun b (TyFun [a] b -> *))
= forall (arg :: b) . KindOf (Apply (Lgo1 l1 l2 l3) arg) ~ KindOf (Lgo2 l1 l2 l3 arg) =>
Lgo1KindInference
type family Lgo f
z0
xs0
(a1 :: b)
(a2 :: [a]) :: b where
Lgo f z0 xs0 z '[] = z
Lgo f z0 xs0 z ('(:) x xs) = Apply (Apply (Lgo1 f z0 xs0) (Apply (Apply f z) x)) xs
```
Note that the above code works fine in GHC 7.10.2.
There are two options to make the code compile on GHC8-rc3:
- Remove the kind annotations on the `forall arg .` binders
- Or make the following changes using TypeInType:
```
{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, UndecidableInstances, TypeInType #-}
module NotInScope where
import Data.Proxy
import GHC.Types
type KindOf (a :: k) = ('KProxy :: KProxy k)
data TyFun :: * -> * -> *
type family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2
data Lgo2 a
b
l1
l2
l3
(l4 :: b)
(l5 :: TyFun [a] b)
= forall (arg :: [a]) . KindOf (Apply (Lgo2 a b l1 l2 l3 l4) arg) ~ KindOf (Lgo a b l1 l2 l3 l4 arg) =>
Lgo2KindInference
data Lgo1 a
b
l1
l2
l3
(l4 :: TyFun b (TyFun [a] b -> *))
= forall (arg :: b) . KindOf (Apply (Lgo1 a b l1 l2 l3) arg) ~ KindOf (Lgo2 a b l1 l2 l3 arg) =>
Lgo1KindInference
type family Lgo a
b
f
z0
xs0
(a1 :: b)
(a2 :: [a]) :: b where
Lgo a b f z0 xs0 z '[] = z
Lgo a b f z0 xs0 z ('(:) x xs) = Apply (Apply (Lgo1 a b f z0 xs0) (Apply (Apply f z) x)) xs
```
I'm sorry I didn't create a smaller test case. Let me know if one is required and I'll try.
The error seems to be related to the recursive aspect of the three definitions and how implicit kind variables are handled in ghc8.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1-rc3 |
| 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":"Internal error: not in scope during type checking, but it passed the renamer","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"While trying to get the singletons package to compile on GHC8 (https://github.com/goldfirere/singletons/pull/142), I encountered the following error while trying to track down a bug:\r\n\r\n{{{\r\n[1 of 1] Compiling NotInScope ( NotInScope.hs, interpreted )\r\n\r\nNotInScope.hs:22:20: error:\r\n • GHC internal error: ‘b’ is not in scope during type checking, but it passed the renamer\r\n tcl_env of environment: [a1lm :-> Type variable ‘b’ = b,\r\n a1lA :-> Type variable ‘l1’ = l1, a1lB :-> Type variable ‘l2’ = l2,\r\n a1lC :-> Type variable ‘l3’ = l3, a1lE :-> Type variable ‘a’ = a,\r\n a1lF :-> Type variable ‘l4’ = l4, r1aq :-> ATcTyCon Lgo,\r\n r1aG :-> ATcTyCon Lgo1, r1aI :-> ATcTyCon Lgo2]\r\n • In the kind ‘b’\r\n In the definition of data constructor ‘Lgo1KindInference’\r\n In the data declaration for ‘Lgo1’\r\n}}}\r\n\r\nfor the following code:\r\n\r\n{{{\r\n{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, UndecidableInstances #-}\r\nmodule NotInScope where\r\n\r\nimport Data.Proxy\r\n\r\ntype KindOf (a :: k) = ('KProxy :: KProxy k)\r\ndata TyFun :: * -> * -> *\r\ntype family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2\r\n\r\ndata Lgo2 l1\r\n l2\r\n l3\r\n (l4 :: b)\r\n (l5 :: TyFun [a] b)\r\n = forall (arg :: [a]) . KindOf (Apply (Lgo2 l1 l2 l3 l4) arg) ~ KindOf (Lgo l1 l2 l3 l4 arg) =>\r\n Lgo2KindInference\r\n\r\ndata Lgo1 l1\r\n l2\r\n l3\r\n (l4 :: TyFun b (TyFun [a] b -> *))\r\n = forall (arg :: b) . KindOf (Apply (Lgo1 l1 l2 l3) arg) ~ KindOf (Lgo2 l1 l2 l3 arg) =>\r\n Lgo1KindInference\r\n\r\ntype family Lgo f\r\n z0\r\n xs0\r\n (a1 :: b)\r\n (a2 :: [a]) :: b where\r\n Lgo f z0 xs0 z '[] = z\r\n Lgo f z0 xs0 z ('(:) x xs) = Apply (Apply (Lgo1 f z0 xs0) (Apply (Apply f z) x)) xs\r\n}}}\r\n\r\nNote that the above code works fine in GHC 7.10.2.\r\n\r\nThere are two options to make the code compile on GHC8-rc3:\r\n* Remove the kind annotations on the {{{forall arg .}}} binders\r\n* Or make the following changes using TypeInType:\r\n\r\n{{{\r\n{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, UndecidableInstances, TypeInType #-}\r\nmodule NotInScope where\r\n\r\nimport Data.Proxy\r\nimport GHC.Types\r\n\r\ntype KindOf (a :: k) = ('KProxy :: KProxy k)\r\ndata TyFun :: * -> * -> *\r\ntype family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2\r\n\r\ndata Lgo2 a\r\n b\r\n l1\r\n l2\r\n l3\r\n (l4 :: b)\r\n (l5 :: TyFun [a] b)\r\n = forall (arg :: [a]) . KindOf (Apply (Lgo2 a b l1 l2 l3 l4) arg) ~ KindOf (Lgo a b l1 l2 l3 l4 arg) =>\r\n Lgo2KindInference\r\n\r\ndata Lgo1 a\r\n b\r\n l1\r\n l2\r\n l3\r\n (l4 :: TyFun b (TyFun [a] b -> *))\r\n = forall (arg :: b) . KindOf (Apply (Lgo1 a b l1 l2 l3) arg) ~ KindOf (Lgo2 a b l1 l2 l3 arg) =>\r\n Lgo1KindInference\r\n\r\ntype family Lgo a\r\n b\r\n f\r\n z0\r\n xs0\r\n (a1 :: b)\r\n (a2 :: [a]) :: b where\r\n Lgo a b f z0 xs0 z '[] = z\r\n Lgo a b f z0 xs0 z ('(:) x xs) = Apply (Apply (Lgo1 a b f z0 xs0) (Apply (Apply f z) x)) xs\r\n}}}\r\n\r\nI'm sorry I didn't create a smaller test case. Let me know if one is required and I'll try.\r\nThe error seems to be related to the recursive aspect of the three definitions and how implicit kind variables are handled in ghc8.","type_of_failure":"OtherFailure","blocking":[]} -->While trying to get the singletons package to compile on GHC8 (https://github.com/goldfirere/singletons/pull/142), I encountered the following error while trying to track down a bug:
```
[1 of 1] Compiling NotInScope ( NotInScope.hs, interpreted )
NotInScope.hs:22:20: error:
• GHC internal error: ‘b’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: [a1lm :-> Type variable ‘b’ = b,
a1lA :-> Type variable ‘l1’ = l1, a1lB :-> Type variable ‘l2’ = l2,
a1lC :-> Type variable ‘l3’ = l3, a1lE :-> Type variable ‘a’ = a,
a1lF :-> Type variable ‘l4’ = l4, r1aq :-> ATcTyCon Lgo,
r1aG :-> ATcTyCon Lgo1, r1aI :-> ATcTyCon Lgo2]
• In the kind ‘b’
In the definition of data constructor ‘Lgo1KindInference’
In the data declaration for ‘Lgo1’
```
for the following code:
```
{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, UndecidableInstances #-}
module NotInScope where
import Data.Proxy
type KindOf (a :: k) = ('KProxy :: KProxy k)
data TyFun :: * -> * -> *
type family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2
data Lgo2 l1
l2
l3
(l4 :: b)
(l5 :: TyFun [a] b)
= forall (arg :: [a]) . KindOf (Apply (Lgo2 l1 l2 l3 l4) arg) ~ KindOf (Lgo l1 l2 l3 l4 arg) =>
Lgo2KindInference
data Lgo1 l1
l2
l3
(l4 :: TyFun b (TyFun [a] b -> *))
= forall (arg :: b) . KindOf (Apply (Lgo1 l1 l2 l3) arg) ~ KindOf (Lgo2 l1 l2 l3 arg) =>
Lgo1KindInference
type family Lgo f
z0
xs0
(a1 :: b)
(a2 :: [a]) :: b where
Lgo f z0 xs0 z '[] = z
Lgo f z0 xs0 z ('(:) x xs) = Apply (Apply (Lgo1 f z0 xs0) (Apply (Apply f z) x)) xs
```
Note that the above code works fine in GHC 7.10.2.
There are two options to make the code compile on GHC8-rc3:
- Remove the kind annotations on the `forall arg .` binders
- Or make the following changes using TypeInType:
```
{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, UndecidableInstances, TypeInType #-}
module NotInScope where
import Data.Proxy
import GHC.Types
type KindOf (a :: k) = ('KProxy :: KProxy k)
data TyFun :: * -> * -> *
type family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2
data Lgo2 a
b
l1
l2
l3
(l4 :: b)
(l5 :: TyFun [a] b)
= forall (arg :: [a]) . KindOf (Apply (Lgo2 a b l1 l2 l3 l4) arg) ~ KindOf (Lgo a b l1 l2 l3 l4 arg) =>
Lgo2KindInference
data Lgo1 a
b
l1
l2
l3
(l4 :: TyFun b (TyFun [a] b -> *))
= forall (arg :: b) . KindOf (Apply (Lgo1 a b l1 l2 l3) arg) ~ KindOf (Lgo2 a b l1 l2 l3 arg) =>
Lgo1KindInference
type family Lgo a
b
f
z0
xs0
(a1 :: b)
(a2 :: [a]) :: b where
Lgo a b f z0 xs0 z '[] = z
Lgo a b f z0 xs0 z ('(:) x xs) = Apply (Apply (Lgo1 a b f z0 xs0) (Apply (Apply f z) x)) xs
```
I'm sorry I didn't create a smaller test case. Let me know if one is required and I'll try.
The error seems to be related to the recursive aspect of the three definitions and how implicit kind variables are handled in ghc8.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1-rc3 |
| 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":"Internal error: not in scope during type checking, but it passed the renamer","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"While trying to get the singletons package to compile on GHC8 (https://github.com/goldfirere/singletons/pull/142), I encountered the following error while trying to track down a bug:\r\n\r\n{{{\r\n[1 of 1] Compiling NotInScope ( NotInScope.hs, interpreted )\r\n\r\nNotInScope.hs:22:20: error:\r\n • GHC internal error: ‘b’ is not in scope during type checking, but it passed the renamer\r\n tcl_env of environment: [a1lm :-> Type variable ‘b’ = b,\r\n a1lA :-> Type variable ‘l1’ = l1, a1lB :-> Type variable ‘l2’ = l2,\r\n a1lC :-> Type variable ‘l3’ = l3, a1lE :-> Type variable ‘a’ = a,\r\n a1lF :-> Type variable ‘l4’ = l4, r1aq :-> ATcTyCon Lgo,\r\n r1aG :-> ATcTyCon Lgo1, r1aI :-> ATcTyCon Lgo2]\r\n • In the kind ‘b’\r\n In the definition of data constructor ‘Lgo1KindInference’\r\n In the data declaration for ‘Lgo1’\r\n}}}\r\n\r\nfor the following code:\r\n\r\n{{{\r\n{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, UndecidableInstances #-}\r\nmodule NotInScope where\r\n\r\nimport Data.Proxy\r\n\r\ntype KindOf (a :: k) = ('KProxy :: KProxy k)\r\ndata TyFun :: * -> * -> *\r\ntype family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2\r\n\r\ndata Lgo2 l1\r\n l2\r\n l3\r\n (l4 :: b)\r\n (l5 :: TyFun [a] b)\r\n = forall (arg :: [a]) . KindOf (Apply (Lgo2 l1 l2 l3 l4) arg) ~ KindOf (Lgo l1 l2 l3 l4 arg) =>\r\n Lgo2KindInference\r\n\r\ndata Lgo1 l1\r\n l2\r\n l3\r\n (l4 :: TyFun b (TyFun [a] b -> *))\r\n = forall (arg :: b) . KindOf (Apply (Lgo1 l1 l2 l3) arg) ~ KindOf (Lgo2 l1 l2 l3 arg) =>\r\n Lgo1KindInference\r\n\r\ntype family Lgo f\r\n z0\r\n xs0\r\n (a1 :: b)\r\n (a2 :: [a]) :: b where\r\n Lgo f z0 xs0 z '[] = z\r\n Lgo f z0 xs0 z ('(:) x xs) = Apply (Apply (Lgo1 f z0 xs0) (Apply (Apply f z) x)) xs\r\n}}}\r\n\r\nNote that the above code works fine in GHC 7.10.2.\r\n\r\nThere are two options to make the code compile on GHC8-rc3:\r\n* Remove the kind annotations on the {{{forall arg .}}} binders\r\n* Or make the following changes using TypeInType:\r\n\r\n{{{\r\n{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, UndecidableInstances, TypeInType #-}\r\nmodule NotInScope where\r\n\r\nimport Data.Proxy\r\nimport GHC.Types\r\n\r\ntype KindOf (a :: k) = ('KProxy :: KProxy k)\r\ndata TyFun :: * -> * -> *\r\ntype family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2\r\n\r\ndata Lgo2 a\r\n b\r\n l1\r\n l2\r\n l3\r\n (l4 :: b)\r\n (l5 :: TyFun [a] b)\r\n = forall (arg :: [a]) . KindOf (Apply (Lgo2 a b l1 l2 l3 l4) arg) ~ KindOf (Lgo a b l1 l2 l3 l4 arg) =>\r\n Lgo2KindInference\r\n\r\ndata Lgo1 a\r\n b\r\n l1\r\n l2\r\n l3\r\n (l4 :: TyFun b (TyFun [a] b -> *))\r\n = forall (arg :: b) . KindOf (Apply (Lgo1 a b l1 l2 l3) arg) ~ KindOf (Lgo2 a b l1 l2 l3 arg) =>\r\n Lgo1KindInference\r\n\r\ntype family Lgo a\r\n b\r\n f\r\n z0\r\n xs0\r\n (a1 :: b)\r\n (a2 :: [a]) :: b where\r\n Lgo a b f z0 xs0 z '[] = z\r\n Lgo a b f z0 xs0 z ('(:) x xs) = Apply (Apply (Lgo1 a b f z0 xs0) (Apply (Apply f z) x)) xs\r\n}}}\r\n\r\nI'm sorry I didn't create a smaller test case. Let me know if one is required and I'll try.\r\nThe error seems to be related to the recursive aspect of the three definitions and how implicit kind variables are handled in ghc8.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.2https://gitlab.haskell.org/ghc/ghc/-/issues/11811GHC sometimes misses a CUSK2019-07-07T18:28:26ZRichard Eisenbergrae@richarde.devGHC sometimes misses a CUSK```
{-# LANGUAGE TypeInType #-}
data Test (a :: x) (b :: x) :: x -> *
where K :: Test Int Bool Double
```
fails, because GHC thinks that `Test` does not have a CUSK.
It should have a CUSK, because while there is no `forall x` in the result kind, the `x` is in scope from previous use in kinds.
Fix en route.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.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":"GHC sometimes misses a CUSK","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{\r\n{-# LANGUAGE TypeInType #-}\r\n\r\ndata Test (a :: x) (b :: x) :: x -> *\r\n where K :: Test Int Bool Double\r\n}}}\r\n\r\nfails, because GHC thinks that `Test` does not have a CUSK.\r\n\r\nIt should have a CUSK, because while there is no `forall x` in the result kind, the `x` is in scope from previous use in kinds.\r\n\r\nFix en route.","type_of_failure":"OtherFailure","blocking":[]} -->```
{-# LANGUAGE TypeInType #-}
data Test (a :: x) (b :: x) :: x -> *
where K :: Test Int Bool Double
```
fails, because GHC thinks that `Test` does not have a CUSK.
It should have a CUSK, because while there is no `forall x` in the result kind, the `x` is in scope from previous use in kinds.
Fix en route.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.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":"GHC sometimes misses a CUSK","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{\r\n{-# LANGUAGE TypeInType #-}\r\n\r\ndata Test (a :: x) (b :: x) :: x -> *\r\n where K :: Test Int Bool Double\r\n}}}\r\n\r\nfails, because GHC thinks that `Test` does not have a CUSK.\r\n\r\nIt should have a CUSK, because while there is no `forall x` in the result kind, the `x` is in scope from previous use in kinds.\r\n\r\nFix en route.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11785Merge types and kinds in Template Haskell2019-07-07T18:28:33ZRichard Eisenbergrae@richarde.devMerge types and kinds in Template Haskell!TcSplice handles kinds differently than types. Now that they are the same, it's probably best to rewrite this code.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ---------------- |
| Version | 8.1 |
| Type | Task |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Template Haskell |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Kinds should be treated like types in TcSplice","status":"New","operating_system":"","component":"Template Haskell","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"!TcSplice handles kinds differently than types. Now that they are the same, it's probably best to rewrite this code.","type_of_failure":"OtherFailure","blocking":[]} -->!TcSplice handles kinds differently than types. Now that they are the same, it's probably best to rewrite this code.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ---------------- |
| Version | 8.1 |
| Type | Task |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Template Haskell |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Kinds should be treated like types in TcSplice","status":"New","operating_system":"","component":"Template Haskell","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"!TcSplice handles kinds differently than types. Now that they are the same, it's probably best to rewrite this code.","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/11754Error in optCoercion2019-07-07T18:28:42ZSimon Peyton JonesError in optCoercionThis program fails Lint after a run of the simplifier.
```hs
{-# LANGUAGE TypeOperators, UndecidableSuperClasses, KindSignatures, TypeFamilies, FlexibleContexts #-}
module T11728a where
import Data.Kind
import Data.Void
newtype K a x = K a
newtype I x = I x
data (f + g) x = L (f x) | R (g x)
data (f × g) x = f x :×: g x
class Differentiable (D f) => Differentiable f where
type D (f :: Type -> Type) :: Type -> Type
instance Differentiable (K a) where
type D (K a) = K Void
instance Differentiable I where
type D I = K ()
instance (Differentiable f₁, Differentiable f₂) => Differentiable (f₁ + f₂) where
type D (f₁ + f₂) = D f₁ + D f₂
instance (Differentiable f₁, Differentiable f₂) => Differentiable (f₁ × f₂) where
type D (f₁ × f₂) = (D f₁ × f₂) + (f₁ × D f₂)
```
Originally reported in #11728, but it's a totally different problem.
Richard has nailed it already... patch coming from him.This program fails Lint after a run of the simplifier.
```hs
{-# LANGUAGE TypeOperators, UndecidableSuperClasses, KindSignatures, TypeFamilies, FlexibleContexts #-}
module T11728a where
import Data.Kind
import Data.Void
newtype K a x = K a
newtype I x = I x
data (f + g) x = L (f x) | R (g x)
data (f × g) x = f x :×: g x
class Differentiable (D f) => Differentiable f where
type D (f :: Type -> Type) :: Type -> Type
instance Differentiable (K a) where
type D (K a) = K Void
instance Differentiable I where
type D I = K ()
instance (Differentiable f₁, Differentiable f₂) => Differentiable (f₁ + f₂) where
type D (f₁ + f₂) = D f₁ + D f₂
instance (Differentiable f₁, Differentiable f₂) => Differentiable (f₁ × f₂) where
type D (f₁ × f₂) = (D f₁ × f₂) + (f₁ × D f₂)
```
Originally reported in #11728, but it's a totally different problem.
Richard has nailed it already... patch coming from him.8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11732Deriving Generic1 interacts poorly with TypeInType2019-07-07T18:28:52ZRichard Eisenbergrae@richarde.devDeriving Generic1 interacts poorly with TypeInTypeFrom \@RyanGlScott, [ticket:11357\#comment:117922](https://gitlab.haskell.org//ghc/ghc/issues/11357#note_117922):
Vanilla datatypes and data family instances are still inconsistent w.r.t. which type variables are considered "instantiated" in a `Generic1` instance. For instance, this is rejected:
```
λ> data Proxy k (a :: k) = ProxyCon deriving Generic1
```
```
<interactive>:32:43: error:
• Can't make a derived instance of ‘Generic1 (Proxy *)’:
Proxy must not be instantiated; try deriving `Proxy k a' instead
• In the data declaration for ‘Proxy’
```
And rightfully so, since the visible kind binder `k` is instantiated to `*`. But now it's possible to have an equivalent instance for a data family that squeaks past this check!
```
λ> data family ProxyFam (a :: y) (b :: z)
λ> data instance ProxyFam k (a :: k) = ProxyFamCon deriving Generic1
==================== Derived instances ====================
Derived instances:
instance GHC.Generics.Generic1 (Ghci13.ProxyFam *) where
...
```
\[Ryan needs\] to investigate further to see why this is the case.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.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":"Deriving Generic1 interacts poorly with TypeInType","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["Generics","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"From @RyanGlScott, comment:9:ticket:11357:\r\n\r\nVanilla datatypes and data family instances are still inconsistent w.r.t. which type variables are considered \"instantiated\" in a `Generic1` instance. For instance, this is rejected:\r\n\r\n{{{\r\nλ> data Proxy k (a :: k) = ProxyCon deriving Generic1\r\n}}}\r\n\r\n{{{\r\n<interactive>:32:43: error:\r\n • Can't make a derived instance of ‘Generic1 (Proxy *)’:\r\n Proxy must not be instantiated; try deriving `Proxy k a' instead\r\n • In the data declaration for ‘Proxy’\r\n}}}\r\n\r\nAnd rightfully so, since the visible kind binder `k` is instantiated to `*`. But now it's possible to have an equivalent instance for a data family that squeaks past this check!\r\n\r\n{{{\r\nλ> data family ProxyFam (a :: y) (b :: z)\r\nλ> data instance ProxyFam k (a :: k) = ProxyFamCon deriving Generic1\r\n\r\n==================== Derived instances ====================\r\nDerived instances:\r\n instance GHC.Generics.Generic1 (Ghci13.ProxyFam *) where\r\n ...\r\n}}}\r\n\r\n[Ryan needs] to investigate further to see why this is the case. ","type_of_failure":"OtherFailure","blocking":[]} -->From \@RyanGlScott, [ticket:11357\#comment:117922](https://gitlab.haskell.org//ghc/ghc/issues/11357#note_117922):
Vanilla datatypes and data family instances are still inconsistent w.r.t. which type variables are considered "instantiated" in a `Generic1` instance. For instance, this is rejected:
```
λ> data Proxy k (a :: k) = ProxyCon deriving Generic1
```
```
<interactive>:32:43: error:
• Can't make a derived instance of ‘Generic1 (Proxy *)’:
Proxy must not be instantiated; try deriving `Proxy k a' instead
• In the data declaration for ‘Proxy’
```
And rightfully so, since the visible kind binder `k` is instantiated to `*`. But now it's possible to have an equivalent instance for a data family that squeaks past this check!
```
λ> data family ProxyFam (a :: y) (b :: z)
λ> data instance ProxyFam k (a :: k) = ProxyFamCon deriving Generic1
==================== Derived instances ====================
Derived instances:
instance GHC.Generics.Generic1 (Ghci13.ProxyFam *) where
...
```
\[Ryan needs\] to investigate further to see why this is the case.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.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":"Deriving Generic1 interacts poorly with TypeInType","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["Generics","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"From @RyanGlScott, comment:9:ticket:11357:\r\n\r\nVanilla datatypes and data family instances are still inconsistent w.r.t. which type variables are considered \"instantiated\" in a `Generic1` instance. For instance, this is rejected:\r\n\r\n{{{\r\nλ> data Proxy k (a :: k) = ProxyCon deriving Generic1\r\n}}}\r\n\r\n{{{\r\n<interactive>:32:43: error:\r\n • Can't make a derived instance of ‘Generic1 (Proxy *)’:\r\n Proxy must not be instantiated; try deriving `Proxy k a' instead\r\n • In the data declaration for ‘Proxy’\r\n}}}\r\n\r\nAnd rightfully so, since the visible kind binder `k` is instantiated to `*`. But now it's possible to have an equivalent instance for a data family that squeaks past this check!\r\n\r\n{{{\r\nλ> data family ProxyFam (a :: y) (b :: z)\r\nλ> data instance ProxyFam k (a :: k) = ProxyFamCon deriving Generic1\r\n\r\n==================== Derived instances ====================\r\nDerived instances:\r\n instance GHC.Generics.Generic1 (Ghci13.ProxyFam *) where\r\n ...\r\n}}}\r\n\r\n[Ryan needs] to investigate further to see why this is the case. ","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/11719Cannot use higher-rank kinds with type families2019-07-07T18:28:55ZOllie CharlesCannot use higher-rank kinds with type familiesThis ticket came out of a discussion with Richard in this mailing list post: https://mail.haskell.org/pipermail/haskell-cafe/2016-March/123462.html
Here's the code that should work, but doesn't:
```hs
import Data.Kind
data TyFun :: * -> * -> *
type a ~> b = TyFun a b -> *
type family (f :: a ~> b) @@ (x :: a) :: b
data Null a = Nullable a | NotNullable a
type family ((f :: b ~> c) ∘ (g :: a ~> b)) (x :: a) :: c where
(f ∘ g) x = f @@ (g @@ x)
type family BaseType (k :: forall a. a ~> Type) (x :: b) :: Type where -- this fails :(
-- BaseType k x = (@@) k x
```This ticket came out of a discussion with Richard in this mailing list post: https://mail.haskell.org/pipermail/haskell-cafe/2016-March/123462.html
Here's the code that should work, but doesn't:
```hs
import Data.Kind
data TyFun :: * -> * -> *
type a ~> b = TyFun a b -> *
type family (f :: a ~> b) @@ (x :: a) :: b
data Null a = Nullable a | NotNullable a
type family ((f :: b ~> c) ∘ (g :: a ~> b)) (x :: a) :: c where
(f ∘ g) x = f @@ (g @@ x)
type family BaseType (k :: forall a. a ~> Type) (x :: b) :: Type where -- this fails :(
-- BaseType k x = (@@) k x
```8.8.1https://gitlab.haskell.org/ghc/ghc/-/issues/11716Make TypeInType stress test work2019-07-07T18:28:57ZRichard Eisenbergrae@richarde.devMake TypeInType stress test workI used the attached file during my job talk. It is good `TypeInType` stress test. This bug is to track several fixes that have been necessary to get it working. I have these fixes locally and will push in due course.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.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":"Make TypeInType stress test work","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I used the attached file during my job talk. It is good `TypeInType` stress test. This bug is to track several fixes that have been necessary to get it working. I have these fixes locally and will push in due course.","type_of_failure":"OtherFailure","blocking":[]} -->I used the attached file during my job talk. It is good `TypeInType` stress test. This bug is to track several fixes that have been necessary to get it working. I have these fixes locally and will push in due course.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.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":"Make TypeInType stress test work","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I used the attached file during my job talk. It is good `TypeInType` stress test. This bug is to track several fixes that have been necessary to get it working. I have these fixes locally and will push in due course.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/11699Type families mistakingly report kind variables as unbound type variables2019-07-07T18:29:02ZmniipType families mistakingly report kind variables as unbound type variablesGHC verifies that if some equation of a type family binds a type variable, that this type variable actually exists and doesn't disappear through type synonym/family application (#7536). However this also mistakingly catches kind variables that aren't present in the type family head.
Simplest test case:
```hs
{-# LANGUAGE TypeFamilies, PolyKinds #-}
type family F a where F (f a) = f a
```
As seen on 8.0.1-rc2 and 7.10.2:
```
../File.hs:3:23:
Family instance purports to bind type variable ‘k1’
but the real LHS (expanding synonyms) is: F (f a) = ...
In the equations for closed type family ‘F’
In the type family declaration for ‘F’
```
The culprit seems to be in `exactTyCoVarsOfType`, which doesn't grab kind variables from a type variable's kind, even though `tyCoVarsOfType` does.
Now, I'm not too sure whether this is a "GHC rejects valid program", or "Incorrect warning at compile time", as I'm not sure if type families like the aforementioned `F` are actually okay. (Are they?)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1-rc2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Type families mistakingly report kind variables as unbound type variables","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC verifies that if some equation of a type family binds a type variable, that this type variable actually exists and doesn't disappear through type synonym/family application (#7536). However this also mistakingly catches kind variables that aren't present in the type family head.\r\n\r\nSimplest test case:\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies, PolyKinds #-}\r\ntype family F a where F (f a) = f a\r\n}}}\r\nAs seen on 8.0.1-rc2 and 7.10.2:\r\n{{{\r\n../File.hs:3:23:\r\n Family instance purports to bind type variable ‘k1’\r\n but the real LHS (expanding synonyms) is: F (f a) = ...\r\n In the equations for closed type family ‘F’\r\n In the type family declaration for ‘F’\r\n}}}\r\n\r\nThe culprit seems to be in `exactTyCoVarsOfType`, which doesn't grab kind variables from a type variable's kind, even though `tyCoVarsOfType` does.\r\n\r\nNow, I'm not too sure whether this is a \"GHC rejects valid program\", or \"Incorrect warning at compile time\", as I'm not sure if type families like the aforementioned `F` are actually okay. (Are they?)","type_of_failure":"OtherFailure","blocking":[]} -->GHC verifies that if some equation of a type family binds a type variable, that this type variable actually exists and doesn't disappear through type synonym/family application (#7536). However this also mistakingly catches kind variables that aren't present in the type family head.
Simplest test case:
```hs
{-# LANGUAGE TypeFamilies, PolyKinds #-}
type family F a where F (f a) = f a
```
As seen on 8.0.1-rc2 and 7.10.2:
```
../File.hs:3:23:
Family instance purports to bind type variable ‘k1’
but the real LHS (expanding synonyms) is: F (f a) = ...
In the equations for closed type family ‘F’
In the type family declaration for ‘F’
```
The culprit seems to be in `exactTyCoVarsOfType`, which doesn't grab kind variables from a type variable's kind, even though `tyCoVarsOfType` does.
Now, I'm not too sure whether this is a "GHC rejects valid program", or "Incorrect warning at compile time", as I'm not sure if type families like the aforementioned `F` are actually okay. (Are they?)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1-rc2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Type families mistakingly report kind variables as unbound type variables","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC verifies that if some equation of a type family binds a type variable, that this type variable actually exists and doesn't disappear through type synonym/family application (#7536). However this also mistakingly catches kind variables that aren't present in the type family head.\r\n\r\nSimplest test case:\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies, PolyKinds #-}\r\ntype family F a where F (f a) = f a\r\n}}}\r\nAs seen on 8.0.1-rc2 and 7.10.2:\r\n{{{\r\n../File.hs:3:23:\r\n Family instance purports to bind type variable ‘k1’\r\n but the real LHS (expanding synonyms) is: F (f a) = ...\r\n In the equations for closed type family ‘F’\r\n In the type family declaration for ‘F’\r\n}}}\r\n\r\nThe culprit seems to be in `exactTyCoVarsOfType`, which doesn't grab kind variables from a type variable's kind, even though `tyCoVarsOfType` does.\r\n\r\nNow, I'm not too sure whether this is a \"GHC rejects valid program\", or \"Incorrect warning at compile time\", as I'm not sure if type families like the aforementioned `F` are actually okay. (Are they?)","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11672Poor error message2019-07-07T18:29:09ZAdam GundryPoor error message[Daniel Díaz recently pointed out](https://mail.haskell.org/pipermail/haskell-cafe/2016-February/123262.html) a particularly terrible error message. Here's a reduced example:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
module BadError where
import GHC.TypeLits
import Data.Proxy
f :: Proxy (a :: Symbol) -> Int
f _ = f (Proxy :: Proxy (Int -> Bool))
```
With GHC 8.0 RC2, this leads to the following error:
```
• Expected kind ‘Proxy ((->) Int Bool)’,
but ‘Data.Proxy.Proxy :: Proxy (Int -> Bool)’ has kind ‘Proxy
(Int -> Bool)’
• In the first argument of ‘f’, namely
‘(Proxy :: Proxy (Int -> Bool))’
In the expression: f (Proxy :: Proxy (Int -> Bool))
In an equation for ‘f’: f _ = f (Proxy :: Proxy (Int -> Bool))
```
or with `-fprint-explicit-kinds -fprint-explicit-coercions`:
```
• Expected kind ‘Proxy
Symbol
(((->) |> <*>_N -> <*>_N -> U(hole:{aCy}, *, Symbol)_N) Int Bool)’,
but ‘(Data.Proxy.Proxy) @ k_aCv @ t_aCw ::
Proxy (Int -> Bool)’ has kind ‘Proxy * (Int -> Bool)’
```
As Iavor, Richard and I discussed, this message has at least three separate problems:
- It says `kind` when it should say `type`.
- `((->) Int Bool)` is printed instead of `Int -> Bool` (because there is a coercion hiding in the type).
- The real error is the insoluble constraint `Symbol ~ *`, which is not reported at all!
The first two should be fairly easy to fix. For the third, when reporting insoluble constraints, we should prefer to report those on which no other constraints depend. (In this case, the presence of `hole:{aCy}` in the constraint is an explicit dependency on the other constraint.)
I'll try to take a look at this. It is no doubt related to #11198.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1-rc2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | diatchki, goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Poor error message","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"adamgundry"},"version":"8.0.1-rc2","keywords":["ErrorMessages"],"differentials":[],"test_case":"","architecture":"","cc":["diatchki","goldfire"],"type":"Bug","description":"[https://mail.haskell.org/pipermail/haskell-cafe/2016-February/123262.html Daniel Díaz recently pointed out] a particularly terrible error message. Here's a reduced example:\r\n{{{#!hs\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE KindSignatures #-}\r\nmodule BadError where\r\n\r\nimport GHC.TypeLits\r\nimport Data.Proxy\r\n\r\nf :: Proxy (a :: Symbol) -> Int\r\nf _ = f (Proxy :: Proxy (Int -> Bool))\r\n}}}\r\n\r\nWith GHC 8.0 RC2, this leads to the following error:\r\n{{{\r\n • Expected kind ‘Proxy ((->) Int Bool)’,\r\n but ‘Data.Proxy.Proxy :: Proxy (Int -> Bool)’ has kind ‘Proxy\r\n (Int -> Bool)’\r\n • In the first argument of ‘f’, namely\r\n ‘(Proxy :: Proxy (Int -> Bool))’\r\n In the expression: f (Proxy :: Proxy (Int -> Bool))\r\n In an equation for ‘f’: f _ = f (Proxy :: Proxy (Int -> Bool))\r\n}}}\r\nor with `-fprint-explicit-kinds -fprint-explicit-coercions`:\r\n{{{\r\n • Expected kind ‘Proxy\r\n Symbol\r\n (((->) |> <*>_N -> <*>_N -> U(hole:{aCy}, *, Symbol)_N) Int Bool)’,\r\n but ‘(Data.Proxy.Proxy) @ k_aCv @ t_aCw ::\r\n Proxy (Int -> Bool)’ has kind ‘Proxy * (Int -> Bool)’\r\n}}}\r\n\r\nAs Iavor, Richard and I discussed, this message has at least three separate problems:\r\n\r\n * It says `kind` when it should say `type`.\r\n\r\n * `((->) Int Bool)` is printed instead of `Int -> Bool` (because there is a coercion hiding in the type).\r\n\r\n * The real error is the insoluble constraint `Symbol ~ *`, which is not reported at all!\r\n\r\nThe first two should be fairly easy to fix. For the third, when reporting insoluble constraints, we should prefer to report those on which no other constraints depend. (In this case, the presence of `hole:{aCy}` in the constraint is an explicit dependency on the other constraint.)\r\n\r\nI'll try to take a look at this. It is no doubt related to #11198.","type_of_failure":"OtherFailure","blocking":[]} -->[Daniel Díaz recently pointed out](https://mail.haskell.org/pipermail/haskell-cafe/2016-February/123262.html) a particularly terrible error message. Here's a reduced example:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
module BadError where
import GHC.TypeLits
import Data.Proxy
f :: Proxy (a :: Symbol) -> Int
f _ = f (Proxy :: Proxy (Int -> Bool))
```
With GHC 8.0 RC2, this leads to the following error:
```
• Expected kind ‘Proxy ((->) Int Bool)’,
but ‘Data.Proxy.Proxy :: Proxy (Int -> Bool)’ has kind ‘Proxy
(Int -> Bool)’
• In the first argument of ‘f’, namely
‘(Proxy :: Proxy (Int -> Bool))’
In the expression: f (Proxy :: Proxy (Int -> Bool))
In an equation for ‘f’: f _ = f (Proxy :: Proxy (Int -> Bool))
```
or with `-fprint-explicit-kinds -fprint-explicit-coercions`:
```
• Expected kind ‘Proxy
Symbol
(((->) |> <*>_N -> <*>_N -> U(hole:{aCy}, *, Symbol)_N) Int Bool)’,
but ‘(Data.Proxy.Proxy) @ k_aCv @ t_aCw ::
Proxy (Int -> Bool)’ has kind ‘Proxy * (Int -> Bool)’
```
As Iavor, Richard and I discussed, this message has at least three separate problems:
- It says `kind` when it should say `type`.
- `((->) Int Bool)` is printed instead of `Int -> Bool` (because there is a coercion hiding in the type).
- The real error is the insoluble constraint `Symbol ~ *`, which is not reported at all!
The first two should be fairly easy to fix. For the third, when reporting insoluble constraints, we should prefer to report those on which no other constraints depend. (In this case, the presence of `hole:{aCy}` in the constraint is an explicit dependency on the other constraint.)
I'll try to take a look at this. It is no doubt related to #11198.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1-rc2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | diatchki, goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Poor error message","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"adamgundry"},"version":"8.0.1-rc2","keywords":["ErrorMessages"],"differentials":[],"test_case":"","architecture":"","cc":["diatchki","goldfire"],"type":"Bug","description":"[https://mail.haskell.org/pipermail/haskell-cafe/2016-February/123262.html Daniel Díaz recently pointed out] a particularly terrible error message. Here's a reduced example:\r\n{{{#!hs\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE KindSignatures #-}\r\nmodule BadError where\r\n\r\nimport GHC.TypeLits\r\nimport Data.Proxy\r\n\r\nf :: Proxy (a :: Symbol) -> Int\r\nf _ = f (Proxy :: Proxy (Int -> Bool))\r\n}}}\r\n\r\nWith GHC 8.0 RC2, this leads to the following error:\r\n{{{\r\n • Expected kind ‘Proxy ((->) Int Bool)’,\r\n but ‘Data.Proxy.Proxy :: Proxy (Int -> Bool)’ has kind ‘Proxy\r\n (Int -> Bool)’\r\n • In the first argument of ‘f’, namely\r\n ‘(Proxy :: Proxy (Int -> Bool))’\r\n In the expression: f (Proxy :: Proxy (Int -> Bool))\r\n In an equation for ‘f’: f _ = f (Proxy :: Proxy (Int -> Bool))\r\n}}}\r\nor with `-fprint-explicit-kinds -fprint-explicit-coercions`:\r\n{{{\r\n • Expected kind ‘Proxy\r\n Symbol\r\n (((->) |> <*>_N -> <*>_N -> U(hole:{aCy}, *, Symbol)_N) Int Bool)’,\r\n but ‘(Data.Proxy.Proxy) @ k_aCv @ t_aCw ::\r\n Proxy (Int -> Bool)’ has kind ‘Proxy * (Int -> Bool)’\r\n}}}\r\n\r\nAs Iavor, Richard and I discussed, this message has at least three separate problems:\r\n\r\n * It says `kind` when it should say `type`.\r\n\r\n * `((->) Int Bool)` is printed instead of `Int -> Bool` (because there is a coercion hiding in the type).\r\n\r\n * The real error is the insoluble constraint `Symbol ~ *`, which is not reported at all!\r\n\r\nThe first two should be fairly easy to fix. For the third, when reporting insoluble constraints, we should prefer to report those on which no other constraints depend. (In this case, the presence of `hole:{aCy}` in the constraint is an explicit dependency on the other constraint.)\r\n\r\nI'll try to take a look at this. It is no doubt related to #11198.","type_of_failure":"OtherFailure","blocking":[]} -->Adam GundryAdam Gundryhttps://gitlab.haskell.org/ghc/ghc/-/issues/11648assertPprPanic, called at compiler/types/TyCoRep.hs:19322019-07-07T18:29:18ZthomieassertPprPanic, called at compiler/types/TyCoRep.hs:1932As mentioned in https://mail.haskell.org/pipermail/ghc-devs/2016-February/011455.html, the following tests currently hit an assert when the compiler is built with -DDEBUG:
```
patsyn/should_compile MoreEx [exit code non-0] (normal)
patsyn/should_compile T11224b [exit code non-0] (normal)
polykinds MonoidsTF [exit code non-0] (normal)
polykinds T11480b [exit code non-0] (normal)
polykinds T11523 [exit code non-0] (normal)
```
```
Compile failed (status 256) errors were:
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.1.20160218 for x86_64-unknown-linux):
ASSERT failed!
CallStack (from HasCallStack):
assertPprPanic, called at compiler/types/TyCoRep.hs:1932:56 in ghc:TyCoRep
checkValidSubst, called at compiler/types/TyCoRep.hs:1991:17 in
ghc:TyCoRep
substTys, called at compiler/types/TyCoRep.hs:2012:14 in ghc:TyCoRep
substTheta, called at compiler/typecheck/TcPatSyn.hs:255:20 in
ghc:TcPatSyn
in_scope InScope {d_ap0 c_apv}
tenv [ap1 :-> c_apv[tau:5]]
tenvFVs [aps :-> t_aps[tau:1], apv :-> c_apv[tau:5]]
cenv []
cenvFVs []
tys []
cos []
```
[D1951](https://phabricator.haskell.org/D1951) contained a stopgap patch, but since it wasn't accepted, I'll just mark the tests as expect_broken for this ticket, so that other developers aren't bothered by this issue.
The offending commit is b5292557dcf2e3844b4837172230575d40a8917e.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.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":"assertPprPanic, called at compiler/types/TyCoRep.hs:1932","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"As mentioned in https://mail.haskell.org/pipermail/ghc-devs/2016-February/011455.html, the following tests currently hit an assert when the compiler is built with -DDEBUG:\r\n\r\n{{{\r\n patsyn/should_compile MoreEx [exit code non-0] (normal)\r\n patsyn/should_compile T11224b [exit code non-0] (normal)\r\n polykinds MonoidsTF [exit code non-0] (normal)\r\n polykinds T11480b [exit code non-0] (normal)\r\n polykinds T11523 [exit code non-0] (normal)\r\n}}}\r\n\r\n{{{\r\nCompile failed (status 256) errors were:\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.1.20160218 for x86_64-unknown-linux):\r\nASSERT failed!\r\n CallStack (from HasCallStack):\r\n assertPprPanic, called at compiler/types/TyCoRep.hs:1932:56 in ghc:TyCoRep\r\n checkValidSubst, called at compiler/types/TyCoRep.hs:1991:17 in\r\nghc:TyCoRep\r\n substTys, called at compiler/types/TyCoRep.hs:2012:14 in ghc:TyCoRep\r\n substTheta, called at compiler/typecheck/TcPatSyn.hs:255:20 in\r\nghc:TcPatSyn\r\n in_scope InScope {d_ap0 c_apv}\r\n tenv [ap1 :-> c_apv[tau:5]]\r\n tenvFVs [aps :-> t_aps[tau:1], apv :-> c_apv[tau:5]]\r\n cenv []\r\n cenvFVs []\r\n tys []\r\n cos []\r\n}}}\r\n\r\nPhab:D1951 contained a stopgap patch, but since it wasn't accepted, I'll just mark the tests as expect_broken for this ticket, so that other developers aren't bothered by this issue.\r\n\r\nThe offending commit is b5292557dcf2e3844b4837172230575d40a8917e.","type_of_failure":"OtherFailure","blocking":[]} -->As mentioned in https://mail.haskell.org/pipermail/ghc-devs/2016-February/011455.html, the following tests currently hit an assert when the compiler is built with -DDEBUG:
```
patsyn/should_compile MoreEx [exit code non-0] (normal)
patsyn/should_compile T11224b [exit code non-0] (normal)
polykinds MonoidsTF [exit code non-0] (normal)
polykinds T11480b [exit code non-0] (normal)
polykinds T11523 [exit code non-0] (normal)
```
```
Compile failed (status 256) errors were:
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.1.20160218 for x86_64-unknown-linux):
ASSERT failed!
CallStack (from HasCallStack):
assertPprPanic, called at compiler/types/TyCoRep.hs:1932:56 in ghc:TyCoRep
checkValidSubst, called at compiler/types/TyCoRep.hs:1991:17 in
ghc:TyCoRep
substTys, called at compiler/types/TyCoRep.hs:2012:14 in ghc:TyCoRep
substTheta, called at compiler/typecheck/TcPatSyn.hs:255:20 in
ghc:TcPatSyn
in_scope InScope {d_ap0 c_apv}
tenv [ap1 :-> c_apv[tau:5]]
tenvFVs [aps :-> t_aps[tau:1], apv :-> c_apv[tau:5]]
cenv []
cenvFVs []
tys []
cos []
```
[D1951](https://phabricator.haskell.org/D1951) contained a stopgap patch, but since it wasn't accepted, I'll just mark the tests as expect_broken for this ticket, so that other developers aren't bothered by this issue.
The offending commit is b5292557dcf2e3844b4837172230575d40a8917e.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.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":"assertPprPanic, called at compiler/types/TyCoRep.hs:1932","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"As mentioned in https://mail.haskell.org/pipermail/ghc-devs/2016-February/011455.html, the following tests currently hit an assert when the compiler is built with -DDEBUG:\r\n\r\n{{{\r\n patsyn/should_compile MoreEx [exit code non-0] (normal)\r\n patsyn/should_compile T11224b [exit code non-0] (normal)\r\n polykinds MonoidsTF [exit code non-0] (normal)\r\n polykinds T11480b [exit code non-0] (normal)\r\n polykinds T11523 [exit code non-0] (normal)\r\n}}}\r\n\r\n{{{\r\nCompile failed (status 256) errors were:\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.1.20160218 for x86_64-unknown-linux):\r\nASSERT failed!\r\n CallStack (from HasCallStack):\r\n assertPprPanic, called at compiler/types/TyCoRep.hs:1932:56 in ghc:TyCoRep\r\n checkValidSubst, called at compiler/types/TyCoRep.hs:1991:17 in\r\nghc:TyCoRep\r\n substTys, called at compiler/types/TyCoRep.hs:2012:14 in ghc:TyCoRep\r\n substTheta, called at compiler/typecheck/TcPatSyn.hs:255:20 in\r\nghc:TcPatSyn\r\n in_scope InScope {d_ap0 c_apv}\r\n tenv [ap1 :-> c_apv[tau:5]]\r\n tenvFVs [aps :-> t_aps[tau:1], apv :-> c_apv[tau:5]]\r\n cenv []\r\n cenvFVs []\r\n tys []\r\n cos []\r\n}}}\r\n\r\nPhab:D1951 contained a stopgap patch, but since it wasn't accepted, I'll just mark the tests as expect_broken for this ticket, so that other developers aren't bothered by this issue.\r\n\r\nThe offending commit is b5292557dcf2e3844b4837172230575d40a8917e.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11642Heterogeneous type equality evidence ignored2019-07-07T18:29:20ZBen GamariHeterogeneous type equality evidence ignoredEither that or I am missing something...
Consider the following,
```hs
{-# LANGUAGE GADTs, PolyKinds, PatternSynonyms, RankNTypes,
TypeOperators, ViewPatterns #-}
module Test where
data TypeRep (a :: k) where
TypeCon :: String -> TypeRep a
TypeApp :: TypeRep f -> TypeRep x -> TypeRep (f x)
data TypeRepX where
TypeRepX :: TypeRep a -> TypeRepX
data (a :: k1) :~~: (b :: k2) where
HRefl :: a :~~: a
trArrow :: TypeRep (->)
trArrow = undefined
eqTypeRep :: TypeRep (a :: k1) -> TypeRep (b :: k2) -> Maybe (a :~~: b)
eqTypeRep = undefined
typeRepKind :: forall (k :: *). forall (a :: k). TypeRep a -> TypeRep k
typeRepKind = undefined
pattern TRFun :: forall fun. ()
=> forall arg res. (fun ~ (arg -> res))
=> TypeRep arg
-> TypeRep res
-> TypeRep fun
pattern TRFun arg res <- TypeApp (TypeApp (eqTypeRep trArrow -> Just HRefl) arg) res
buildApp :: TypeRepX -> TypeRepX -> TypeRepX
buildApp (TypeRepX f) (TypeRepX x) =
case typeRepKind f of
TRFun arg _ ->
case eqTypeRep arg x of
Just HRefl ->
TypeRepX $ TypeApp f x
```
This fails with,
```
$ ghc Test.hs -fprint-explicit-kinds
[1 of 1] Compiling Test ( Test.hs, Test.o )
Test.hs:38:30: error:
• Expected kind ‘TypeRep (k1 -> res) a’,
but ‘f’ has kind ‘TypeRep k a’
• In the first argument of ‘TypeApp’, namely ‘f’
In the second argument of ‘($)’, namely ‘TypeApp f x’
In the expression: TypeRepX $ TypeApp f x
• Relevant bindings include
arg :: TypeRep * arg (bound at Test.hs:35:11)
```
That is, the typechecker doesn't believe that `f`'s type (why is it saying "kind" here?), `TypeRep k a`, will unify with `TypeRep (k1 -> res) a`, despite the `TRFun` pattern match, which should have brought into scope that `k ~ (arg -> res)`.
This was tested with a recent snapshot from `ghc-8.0` (23baff798aca5856650508ad0f7727045efe3680).
Am I missing something here or is this a bug?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Typechecker doesn't use evidence available from pattern synonym?","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Either that or I am missing something...\r\n\r\nConsider the following,\r\n{{{#!hs\r\n{-# LANGUAGE GADTs, PolyKinds, PatternSynonyms, RankNTypes,\r\n TypeOperators, ViewPatterns #-}\r\n\r\nmodule Test where\r\n\r\ndata TypeRep (a :: k) where\r\n TypeCon :: String -> TypeRep a\r\n TypeApp :: TypeRep f -> TypeRep x -> TypeRep (f x)\r\n\r\ndata TypeRepX where\r\n TypeRepX :: TypeRep a -> TypeRepX\r\n\r\ndata (a :: k1) :~~: (b :: k2) where\r\n HRefl :: a :~~: a\r\n\r\ntrArrow :: TypeRep (->)\r\ntrArrow = undefined\r\n\r\neqTypeRep :: TypeRep (a :: k1) -> TypeRep (b :: k2) -> Maybe (a :~~: b)\r\neqTypeRep = undefined\r\n\r\ntypeRepKind :: forall (k :: *). forall (a :: k). TypeRep a -> TypeRep k\r\ntypeRepKind = undefined\r\n\r\npattern TRFun :: forall fun. ()\r\n => forall arg res. (fun ~ (arg -> res))\r\n => TypeRep arg\r\n -> TypeRep res\r\n -> TypeRep fun\r\npattern TRFun arg res <- TypeApp (TypeApp (eqTypeRep trArrow -> Just HRefl) arg) res\r\n\r\nbuildApp :: TypeRepX -> TypeRepX -> TypeRepX\r\nbuildApp (TypeRepX f) (TypeRepX x) =\r\n case typeRepKind f of\r\n TRFun arg _ ->\r\n case eqTypeRep arg x of\r\n Just HRefl ->\r\n TypeRepX $ TypeApp f x\r\n}}}\r\n\r\nThis fails with,\r\n{{{\r\n$ ghc Test.hs -fprint-explicit-kinds\r\n[1 of 1] Compiling Test ( Test.hs, Test.o )\r\n\r\nTest.hs:38:30: error:\r\n • Expected kind ‘TypeRep (k1 -> res) a’,\r\n but ‘f’ has kind ‘TypeRep k a’\r\n • In the first argument of ‘TypeApp’, namely ‘f’\r\n In the second argument of ‘($)’, namely ‘TypeApp f x’\r\n In the expression: TypeRepX $ TypeApp f x\r\n • Relevant bindings include\r\n arg :: TypeRep * arg (bound at Test.hs:35:11)\r\n}}}\r\n\r\nThat is, the typechecker doesn't believe that `f`'s type (why is it saying \"kind\" here?), `TypeRep k a`, will unify with `TypeRep (k1 -> res) a`, despite the `TRFun` pattern match, which should have brought into scope that `k ~ (arg -> res)`.\r\n\r\nThis was tested with a recent snapshot from `ghc-8.0` (23baff798aca5856650508ad0f7727045efe3680).\r\n\r\nAm I missing something here or is this a bug?","type_of_failure":"OtherFailure","blocking":[]} -->Either that or I am missing something...
Consider the following,
```hs
{-# LANGUAGE GADTs, PolyKinds, PatternSynonyms, RankNTypes,
TypeOperators, ViewPatterns #-}
module Test where
data TypeRep (a :: k) where
TypeCon :: String -> TypeRep a
TypeApp :: TypeRep f -> TypeRep x -> TypeRep (f x)
data TypeRepX where
TypeRepX :: TypeRep a -> TypeRepX
data (a :: k1) :~~: (b :: k2) where
HRefl :: a :~~: a
trArrow :: TypeRep (->)
trArrow = undefined
eqTypeRep :: TypeRep (a :: k1) -> TypeRep (b :: k2) -> Maybe (a :~~: b)
eqTypeRep = undefined
typeRepKind :: forall (k :: *). forall (a :: k). TypeRep a -> TypeRep k
typeRepKind = undefined
pattern TRFun :: forall fun. ()
=> forall arg res. (fun ~ (arg -> res))
=> TypeRep arg
-> TypeRep res
-> TypeRep fun
pattern TRFun arg res <- TypeApp (TypeApp (eqTypeRep trArrow -> Just HRefl) arg) res
buildApp :: TypeRepX -> TypeRepX -> TypeRepX
buildApp (TypeRepX f) (TypeRepX x) =
case typeRepKind f of
TRFun arg _ ->
case eqTypeRep arg x of
Just HRefl ->
TypeRepX $ TypeApp f x
```
This fails with,
```
$ ghc Test.hs -fprint-explicit-kinds
[1 of 1] Compiling Test ( Test.hs, Test.o )
Test.hs:38:30: error:
• Expected kind ‘TypeRep (k1 -> res) a’,
but ‘f’ has kind ‘TypeRep k a’
• In the first argument of ‘TypeApp’, namely ‘f’
In the second argument of ‘($)’, namely ‘TypeApp f x’
In the expression: TypeRepX $ TypeApp f x
• Relevant bindings include
arg :: TypeRep * arg (bound at Test.hs:35:11)
```
That is, the typechecker doesn't believe that `f`'s type (why is it saying "kind" here?), `TypeRep k a`, will unify with `TypeRep (k1 -> res) a`, despite the `TRFun` pattern match, which should have brought into scope that `k ~ (arg -> res)`.
This was tested with a recent snapshot from `ghc-8.0` (23baff798aca5856650508ad0f7727045efe3680).
Am I missing something here or is this a bug?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Typechecker doesn't use evidence available from pattern synonym?","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Either that or I am missing something...\r\n\r\nConsider the following,\r\n{{{#!hs\r\n{-# LANGUAGE GADTs, PolyKinds, PatternSynonyms, RankNTypes,\r\n TypeOperators, ViewPatterns #-}\r\n\r\nmodule Test where\r\n\r\ndata TypeRep (a :: k) where\r\n TypeCon :: String -> TypeRep a\r\n TypeApp :: TypeRep f -> TypeRep x -> TypeRep (f x)\r\n\r\ndata TypeRepX where\r\n TypeRepX :: TypeRep a -> TypeRepX\r\n\r\ndata (a :: k1) :~~: (b :: k2) where\r\n HRefl :: a :~~: a\r\n\r\ntrArrow :: TypeRep (->)\r\ntrArrow = undefined\r\n\r\neqTypeRep :: TypeRep (a :: k1) -> TypeRep (b :: k2) -> Maybe (a :~~: b)\r\neqTypeRep = undefined\r\n\r\ntypeRepKind :: forall (k :: *). forall (a :: k). TypeRep a -> TypeRep k\r\ntypeRepKind = undefined\r\n\r\npattern TRFun :: forall fun. ()\r\n => forall arg res. (fun ~ (arg -> res))\r\n => TypeRep arg\r\n -> TypeRep res\r\n -> TypeRep fun\r\npattern TRFun arg res <- TypeApp (TypeApp (eqTypeRep trArrow -> Just HRefl) arg) res\r\n\r\nbuildApp :: TypeRepX -> TypeRepX -> TypeRepX\r\nbuildApp (TypeRepX f) (TypeRepX x) =\r\n case typeRepKind f of\r\n TRFun arg _ ->\r\n case eqTypeRep arg x of\r\n Just HRefl ->\r\n TypeRepX $ TypeApp f x\r\n}}}\r\n\r\nThis fails with,\r\n{{{\r\n$ ghc Test.hs -fprint-explicit-kinds\r\n[1 of 1] Compiling Test ( Test.hs, Test.o )\r\n\r\nTest.hs:38:30: error:\r\n • Expected kind ‘TypeRep (k1 -> res) a’,\r\n but ‘f’ has kind ‘TypeRep k a’\r\n • In the first argument of ‘TypeApp’, namely ‘f’\r\n In the second argument of ‘($)’, namely ‘TypeApp f x’\r\n In the expression: TypeRepX $ TypeApp f x\r\n • Relevant bindings include\r\n arg :: TypeRep * arg (bound at Test.hs:35:11)\r\n}}}\r\n\r\nThat is, the typechecker doesn't believe that `f`'s type (why is it saying \"kind\" here?), `TypeRep k a`, will unify with `TypeRep (k1 -> res) a`, despite the `TRFun` pattern match, which should have brought into scope that `k ~ (arg -> res)`.\r\n\r\nThis was tested with a recent snapshot from `ghc-8.0` (23baff798aca5856650508ad0f7727045efe3680).\r\n\r\nAm I missing something here or is this a bug?","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.dev