GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20200427T10:20:56Zhttps://gitlab.haskell.org/ghc/ghc//issues/18062A cast might get in the way of instantiation20200427T10:20:56ZSimon Peyton JonesA cast might get in the way of instantiationSuppose we have a type signature `f :: forall a. Eq a => blah`, and it somehow kindchecks to
```
forall a. ((Eq a => Blah) > co)
```
In principle this can happen:
```
tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) ...Suppose we have a type signature `f :: forall a. Eq a => blah`, and it somehow kindchecks to
```
forall a. ((Eq a => Blah) > co)
```
In principle this can happen:
```
tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind
= do { ctxt' < tc_hs_context mode ctxt
; ek < newOpenTypeKind  The body kind (result of the function) can
 be TYPE r, for any r, hence newOpenTypeKind
; ty' < tc_lhs_type mode rn_ty ek
; checkExpectedKind (unLoc rn_ty) (mkPhiTy ctxt' ty')
liftedTypeKind exp_kind }
```
That `checkExpectedKind` can add a cast.
If this happens, our instantiation mechanisms would fall over in a heap. We'd instantiate the `forall a`, but then fail to instantiate the `Eq a =>`; instead we'd unify `(Eq a => blah) > co` with the function body. Bad, bad.
This popped up when fixing #18008, when a missing zonk in `tcHsPartialSigType` was producing just such a forall (with a Refl coercion). But it seems plausible that it could happen for real.
EDIT: And it does:
```hs
{# LANGUAGE KindSignatures, TypeFamilies, DataKinds #}
module Bug where
import Data.Kind ( Type )
type family Star where
Star = Type
f :: ((Eq a => a > Bool) :: Star)
f x = x == x
```
produces
```
Bug.hs:11:1: error:
• Couldn't match kind ‘Constraint’ with ‘*’
When matching types
a0 :: *
Eq a :: Constraint
Expected type: Eq a => a > Bool
Actual type: a0 > Bool
• The equation(s) for ‘f’ have one argument,
but its type ‘Eq a => a > Bool’ has none
• Relevant bindings include
f :: Eq a => a > Bool (bound at Bug.hs:11:1)

11  f x = x == x
 ^^^^^^^^^^^^
```
Solution: teach instantiation to look through casts.https://gitlab.haskell.org/ghc/ghc//issues/17327Kindchecking associated types20200218T16:17:45ZmniipKindchecking associated types## Summary
When kind checking associated type declarations in an `instance` declaration, the instance context seems to be ignored.
## Steps to reproduce
Minimal complete example:
```haskell
{# LANGUAGE DataKinds, PolyKinds, TypeFamil...## Summary
When kind checking associated type declarations in an `instance` declaration, the instance context seems to be ignored.
## Steps to reproduce
Minimal complete example:
```haskell
{# LANGUAGE DataKinds, PolyKinds, TypeFamilies, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, TypeApplications #}
class C (k :: *) (a :: *) where
type F k a :: k
data D k (x :: k)
instance C k (D k x) where
type F k (D k x) = x  good
instance (k ~ l) => C l (D k x) where
type F l (D k x) = x  bad
{
b.hs:11:22: error:
• Expected kind ‘l’, but ‘x’ has kind ‘k’
• In the type ‘x’
In the type instance declaration for ‘F’
In the instance declaration for ‘C l (D k x)’

11  type F l (D k x) = x  bad
 ^
}
```
## Expected behavior
The second instance should kindcheck (it has better instance resolution properties than the first which is why we want it).
## Environment
Tested on GHC 8.6.5 and GHC HEADhttps://gitlab.haskell.org/ghc/ghc//issues/14155GHC mentions unlifted types out of the blue (to me anyway)20200123T19:31:01ZIcelandjackGHC mentions unlifted types out of the blue (to me anyway)This one does me 'ead in, I accidentally type `Ran` instead of `Swap`
```hs
{# Language RankNTypes, DerivingStrategies, TypeApplications, ScopedTypeVariables, GADTs, GeneralizedNewtypeDeriving, InstanceSigs, PolyKinds #}
import Data....This one does me 'ead in, I accidentally type `Ran` instead of `Swap`
```hs
{# Language RankNTypes, DerivingStrategies, TypeApplications, ScopedTypeVariables, GADTs, GeneralizedNewtypeDeriving, InstanceSigs, PolyKinds #}
import Data.Coerce
newtype Ran g h a = Ran (forall b. (a > g b) > h b)
newtype Swap p f g a where
Swap :: p g f a > Swap p f g a
deriving newtype
Show
class IxPointed m where
ireturn :: a > m i i a
instance IxPointed f => IxPointed (Swap f) where
ireturn :: forall a i. a > Swap f i i a
ireturn a = Ran (ireturn a)
```
and get this error
```
$ ghci ignoredotghci /tmp/bug.hs
GHCi, version 8.3.20170605: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /tmp/bug.hs, interpreted )
/tmp/bug.hs:17:15: error:
• Couldn't match expected type ‘Swap f i i a’
with actual type ‘Ran g0 h0 a0’
• In the expression: Ran (ireturn a)
In an equation for ‘ireturn’: ireturn a = Ran (ireturn a)
In the instance declaration for ‘IxPointed (Swap f)’
• Relevant bindings include
a :: a (bound at /tmp/bug.hs:17:11)
ireturn :: a > Swap f i i a (bound at /tmp/bug.hs:17:3)

17  ireturn a = Ran (ireturn a)
 ^^^^^^^^^^^^^^^
/tmp/bug.hs:17:20: error:
• Couldn't match a lifted type with an unlifted type
Expected type: (a0 > g0 b) > h0 b
Actual type: (>) (a0 > g0 b) (a0 > g0 b) a
• In the first argument of ‘Ran’, namely ‘(ireturn a)’
In the expression: Ran (ireturn a)
In an equation for ‘ireturn’: ireturn a = Ran (ireturn a)

17  ireturn a = Ran (ireturn a)
 ^^^^^^^^^
Failed, modules loaded: none.
```
Is GHC right to bring up unlifted types? I would guess this is due to the newly added levity polymorphism of `(>) :: TYPE rep > TYPE rep' > Type`
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.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 mentions unlifted types out of the blue (to me anyway)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This one does me 'ead in, I accidentally type `Ran` instead of `Swap` \r\n\r\n{{{#!hs\r\n{# Language RankNTypes, DerivingStrategies, TypeApplications, ScopedTypeVariables, GADTs, GeneralizedNewtypeDeriving, InstanceSigs, PolyKinds #}\r\n\r\nimport Data.Coerce\r\n\r\nnewtype Ran g h a = Ran (forall b. (a > g b) > h b)\r\n\r\nnewtype Swap p f g a where\r\n Swap :: p g f a > Swap p f g a\r\n deriving newtype\r\n Show\r\n\r\nclass IxPointed m where\r\n ireturn :: a > m i i a\r\n\r\ninstance IxPointed f => IxPointed (Swap f) where\r\n ireturn :: forall a i. a > Swap f i i a\r\n ireturn a = Ran (ireturn a)\r\n}}}\r\n\r\nand get this error\r\n\r\n{{{\r\n$ ghci ignoredotghci /tmp/bug.hs\r\nGHCi, version 8.3.20170605: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /tmp/bug.hs, interpreted )\r\n\r\n/tmp/bug.hs:17:15: error:\r\n • Couldn't match expected type ‘Swap f i i a’\r\n with actual type ‘Ran g0 h0 a0’\r\n • In the expression: Ran (ireturn a)\r\n In an equation for ‘ireturn’: ireturn a = Ran (ireturn a)\r\n In the instance declaration for ‘IxPointed (Swap f)’\r\n • Relevant bindings include\r\n a :: a (bound at /tmp/bug.hs:17:11)\r\n ireturn :: a > Swap f i i a (bound at /tmp/bug.hs:17:3)\r\n \r\n17  ireturn a = Ran (ireturn a)\r\n  ^^^^^^^^^^^^^^^\r\n\r\n/tmp/bug.hs:17:20: error:\r\n • Couldn't match a lifted type with an unlifted type\r\n Expected type: (a0 > g0 b) > h0 b\r\n Actual type: (>) (a0 > g0 b) (a0 > g0 b) a\r\n • In the first argument of ‘Ran’, namely ‘(ireturn a)’\r\n In the expression: Ran (ireturn a)\r\n In an equation for ‘ireturn’: ireturn a = Ran (ireturn a)\r\n \r\n17  ireturn a = Ran (ireturn a)\r\n  ^^^^^^^^^\r\nFailed, modules loaded: none.\r\n}}}\r\n\r\nIs GHC right to bring up unlifted types? I would guess this is due to the newly added levity polymorphism of `(>) :: TYPE rep > TYPE rep' > Type`","type_of_failure":"OtherFailure","blocking":[]} >Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/14319Stuck type families can lead to lousy error messages20200123T19:27:40ZDavid FeuerStuck type families can lead to lousy error messagesI first noticed this problem at the type level:
```hs
{# language TypeFamilies, TypeInType, ScopedTypeVariables #}
module ArityError where
import Data.Kind
import GHC.TypeLits
import Data.Proxy
type family F (s :: Symbol) :: Type
ty...I first noticed this problem at the type level:
```hs
{# language TypeFamilies, TypeInType, ScopedTypeVariables #}
module ArityError where
import Data.Kind
import GHC.TypeLits
import Data.Proxy
type family F (s :: Symbol) :: Type
type family G (s :: Symbol) :: F s
type instance G "Hi" = Maybe
```
This produces the error message
```hs
ArityError.hs:10:24: error:
• Expecting one more argument to ‘Maybe’
Expected kind ‘F "Hi"’, but ‘Maybe’ has kind ‘* > *’
• In the type ‘Maybe’
In the type instance declaration for ‘G’

10  type instance G "Hi" = Maybe
 ^^^^^
```
This looks utterly bogus: `F "Hi"` is stuck, so we have no idea what arity it indicates.

I just realized we have a similar problem at the term level:
```hs
f :: forall (s :: Symbol). Proxy s > F s
f _ _ = undefined
```
produces
```hs
ArityError.hs:14:1: error:
• Couldn't match expected type ‘F s’ with actual type ‘p0 > a0’
The type variables ‘p0’, ‘a0’ are ambiguous
• The equation(s) for ‘f’ have two arguments,
but its type ‘Proxy s > F s’ has only one
• Relevant bindings include
f :: Proxy s > F s (bound at ArityError.hs:14:1)

14  f _ _ = undefined
 ^^^^^^^^^^^^^^^^^
```
The claim that `Proxy s > F s` has only one argument is bogus; we only know that it has *at least* one argument. The fix (I imagine) is to refrain from reporting arity errors when we don't know enough about the relevant arities.https://gitlab.haskell.org/ghc/ghc//issues/17621Typelevel multiplication parsed as application at kind *, no guidance provided20200105T03:00:19ZGeshTypelevel multiplication parsed as application at kind *, no guidance provided## Summary
Location of documentation issue: GHC error message
To reproduce:
```
Prelude> :set XDataKinds XTypeOperators
Prelude> import GHC.TypeNats
Prelude GHC.TypeNats> :k 2 * 4
<interactive>:1:1: error:
• Expected kind ‘* >...## Summary
Location of documentation issue: GHC error message
To reproduce:
```
Prelude> :set XDataKinds XTypeOperators
Prelude> import GHC.TypeNats
Prelude GHC.TypeNats> :k 2 * 4
<interactive>:1:1: error:
• Expected kind ‘* > GHC.Types.Nat > k0’,
but ‘2’ has kind ‘GHC.Types.Nat’
• In the type ‘2 * 4’
```
The error message is correct, but useless for someone getting started working
at the type level. At the very least, a suggestion of adding ```NoStarIsType```
is in order.
## Proposed improvements or changes
In a kinding error of form "expected ```* > r```, found ```s```" with
```StarInType```, suggest that this error might be the due to ```StarInType```.
## Environment
* GHC version used (if appropriate): 8.6.5. Asked on IRC, and @solonarv checked
this still exists in 8.8https://gitlab.haskell.org/ghc/ghc//issues/16635Scoped kind variables are broken20190925T18:06:23ZVladislav ZavialovScoped kind variables are broken# Summary
This does work:
```haskell
 f :: [a > Either a ()]
f = [Left @a :: forall a. a > Either a ()]
````
This does not:
```haskell
 type F :: [a > Either a ()]
type F = '[Left @a :: forall a. a > Either a ()]
```
An unfo...# Summary
This does work:
```haskell
 f :: [a > Either a ()]
f = [Left @a :: forall a. a > Either a ()]
````
This does not:
```haskell
 type F :: [a > Either a ()]
type F = '[Left @a :: forall a. a > Either a ()]
```
An unfortunate asymmetry between terms & types. See a related discussion at https://gitlab.haskell.org/ghc/ghc/wikis/ghckinds/kindinference/tlks
# Steps to reproduce
```
ghci> :set XScopedTypeVariables XDataKinds XPolyKinds XTypeApplications
ghci> type F = '[Left @a :: forall a. a > Either a ()]
<interactive>:3:18: error: Not in scope: type variable ‘a’
```
# Expected behavior
No error.
# Environment
* GHC version used: HEAD.Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc//issues/12564Type family in type pattern kind20190824T18:45:27ZVladislav ZavialovType family in type pattern kindI want to write a type family that is analogous to `!!` for lists but requires the index to be no bigger than the length of the list. Usually, in dependently typed languages finite sets are used for this purpose, here's an attempt to do ...I want to write a type family that is analogous to `!!` for lists but requires the index to be no bigger than the length of the list. Usually, in dependently typed languages finite sets are used for this purpose, here's an attempt to do so in Haskell:
```haskell
{# LANGUAGE TypeInType, TypeFamilies, GADTs, TypeOperators #}
import Data.Kind
data N = Z  S N
type family Len (xs :: [a]) :: N where
Len '[] = Z
Len (_ ': xs) = S (Len xs)
data Fin :: N > Type where
FZ :: Fin (S n)
FS :: Fin n > Fin (S n)
type family At (xs :: [a]) (i :: Fin (Len xs)) :: a where
At (x ': _) FZ = x
At (_ ': xs) (FS i) = At xs i
```
It fails to compile with this error:
```
FinAt.hs:16:3: error:
• Illegal type synonym family application in instance: 'FZ
• In the equations for closed type family ‘At’
In the type family declaration for ‘At’
```
That's because the kind of the `FZ` pattern (first clause of `At`) has the kind `Fin (Len xs)` and the application of `Len` cannot reduce completely. `checkValidTypePat` then disallows the pattern, as it contains a type family application.
I tried to suppress `checkValidTypePat` and the definition of `At` has compiled; however, it's of little use, since `At` doesn't reduce:
```haskell
x :: At '[Bool] FZ
x = True
```
results in
```
FinAt.hs:20:5: error:
• Couldn't match expected type ‘At
* ((':) * Bool ('[] *)) ('FZ 'Z)’
with actual type ‘Bool’
• In the expression: True
In an equation for ‘x’: x = True
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  goldfire, intindex 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Type family in type pattern kind","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire","intindex"],"type":"Bug","description":"I want to write a type family that is analogous to `!!` for lists but requires the index to be no bigger than the length of the list. Usually, in dependently typed languages finite sets are used for this purpose, here's an attempt to do so in Haskell:\r\n\r\n{{{#!haskell\r\n{# LANGUAGE TypeInType, TypeFamilies, GADTs, TypeOperators #}\r\n\r\nimport Data.Kind\r\n\r\ndata N = Z  S N\r\n\r\ntype family Len (xs :: [a]) :: N where\r\n Len '[] = Z\r\n Len (_ ': xs) = S (Len xs)\r\n\r\ndata Fin :: N > Type where\r\n FZ :: Fin (S n)\r\n FS :: Fin n > Fin (S n)\r\n\r\ntype family At (xs :: [a]) (i :: Fin (Len xs)) :: a where\r\n At (x ': _) FZ = x\r\n At (_ ': xs) (FS i) = At xs i\r\n}}}\r\n\r\nIt fails to compile with this error:\r\n\r\n{{{\r\nFinAt.hs:16:3: error:\r\n • Illegal type synonym family application in instance: 'FZ\r\n • In the equations for closed type family ‘At’\r\n In the type family declaration for ‘At’\r\n}}}\r\n\r\nThat's because the kind of the `FZ` pattern (first clause of `At`) has the kind `Fin (Len xs)` and the application of `Len` cannot reduce completely. `checkValidTypePat` then disallows the pattern, as it contains a type family application.\r\n\r\nI tried to suppress `checkValidTypePat` and the definition of `At` has compiled; however, it's of little use, since `At` doesn't reduce:\r\n\r\n{{{#!haskell\r\nx :: At '[Bool] FZ\r\nx = True\r\n}}}\r\n\r\nresults in\r\n\r\n{{{\r\nFinAt.hs:20:5: error:\r\n • Couldn't match expected type ‘At\r\n * ((':) * Bool ('[] *)) ('FZ 'Z)’\r\n with actual type ‘Bool’\r\n • In the expression: True\r\n In an equation for ‘x’: x = True\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.4.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/7503Bug with PolyKinds, type synonyms & GADTs20190707T18:49:28ZAshley YakeleyBug with PolyKinds, type synonyms & GADTsGHC incorrectly rejects this program:
```
{# LANGUAGE ExistentialQuantification, DataKinds, PolyKinds, KindSignatures, GADTs #}
module TestConstraintKinds where
import GHC.Exts hiding (Any)
data WrappedType = forall a. WrapTy...GHC incorrectly rejects this program:
```
{# LANGUAGE ExistentialQuantification, DataKinds, PolyKinds, KindSignatures, GADTs #}
module TestConstraintKinds where
import GHC.Exts hiding (Any)
data WrappedType = forall a. WrapType a
data A :: WrappedType > * where
MkA :: forall (a :: *). AW a > A (WrapType a)
type AW (a :: k) = A (WrapType a)
type AW' (a :: k) = A (WrapType a)
class C (a :: k) where
aw :: AW a  workaround: AW'
instance C [] where
aw = aw
```
GHC accepts the program when AW is replaced with AW' on that line.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.6.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Bug with PolyKinds, type synonyms & GADTs","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.6.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC incorrectly rejects this program:\r\n{{{\r\n{# LANGUAGE ExistentialQuantification, DataKinds, PolyKinds, KindSignatures, GADTs #}\r\nmodule TestConstraintKinds where\r\n import GHC.Exts hiding (Any)\r\n\r\n data WrappedType = forall a. WrapType a\r\n\r\n data A :: WrappedType > * where\r\n MkA :: forall (a :: *). AW a > A (WrapType a)\r\n\r\n type AW (a :: k) = A (WrapType a)\r\n type AW' (a :: k) = A (WrapType a)\r\n\r\n class C (a :: k) where\r\n aw :: AW a  workaround: AW'\r\n\r\n instance C [] where\r\n aw = aw\r\n}}}\r\n\r\nGHC accepts the program when AW is replaced with AW' on that line.","type_of_failure":"OtherFailure","blocking":[]} >8.0.1Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc//issues/12612Allow kinds of associated types to depend on earlier associated types20190707T18:25:50ZdavemenendezAllow kinds of associated types to depend on earlier associated typesGHC rejects the following code:
```hs
class C t where
type K t :: Type
type T t :: K t > Type
m :: t > T t a
```
with this error message
```
• Type constructor ‘K’ cannot be used here
(it is defined and used...GHC rejects the following code:
```hs
class C t where
type K t :: Type
type T t :: K t > Type
m :: t > T t a
```
with this error message
```
• Type constructor ‘K’ cannot be used here
(it is defined and used in the same recursive group)
• In the kind ‘K t > Type’
```
See [email discussion](https://mail.haskell.org/pipermail/glasgowhaskellusers/2016September/026402.html). This is connected to #12088, at least as far as defining instances of C.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Allow kinds of associated types to depend on earlier associated types","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC rejects the following code:\r\n\r\n{{{#!hs\r\nclass C t where\r\n type K t :: Type\r\n type T t :: K t > Type\r\n\r\n m :: t > T t a\r\n}}}\r\n\r\nwith this error message\r\n\r\n{{{\r\n • Type constructor ‘K’ cannot be used here\r\n (it is defined and used in the same recursive group)\r\n • In the kind ‘K t > Type’\r\n}}}\r\n\r\nSee [https://mail.haskell.org/pipermail/glasgowhaskellusers/2016September/026402.html email discussion]. This is connected to #12088, at least as far as defining instances of C.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/13933Support Typeable instances for types with coercions20190707T18:19:21ZRichard Eisenbergrae@richarde.devSupport Typeable instances for types with coercionsIf I say
```hs
{# LANGUAGE GADTs, TypeApplications, TypeInType #}
module Bug where
import Type.Reflection
data G a where
MkG :: a ~ Bool => G a
rep = typeRep @MkG
```
I get
```
Bug.hs:10:7: error:
• No instance for (Typeab...If I say
```hs
{# LANGUAGE GADTs, TypeApplications, TypeInType #}
module Bug where
import Type.Reflection
data G a where
MkG :: a ~ Bool => G a
rep = typeRep @MkG
```
I get
```
Bug.hs:10:7: error:
• No instance for (Typeable <>) arising from a use of ‘typeRep’
• In the expression: typeRep @MkG
In an equation for ‘rep’: rep = typeRep @MkG

10  rep = typeRep @MkG

```
First off, the error message is confusing, mentioning the mysterious `<>`. But more importantly, it would be nice if the `Typeable` mechanism supported coercions.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.3 
 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":"Support Typeable instances for types with coercions","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["TypeInType,","Typeable"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If I say\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs, TypeApplications, TypeInType #}\r\n\r\nmodule Bug where\r\n\r\nimport Type.Reflection\r\n\r\ndata G a where\r\n MkG :: a ~ Bool => G a\r\n\r\nrep = typeRep @MkG\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\nBug.hs:10:7: error:\r\n • No instance for (Typeable <>) arising from a use of ‘typeRep’\r\n • In the expression: typeRep @MkG\r\n In an equation for ‘rep’: rep = typeRep @MkG\r\n \r\n10  rep = typeRep @MkG\r\n  \r\n}}}\r\n\r\nFirst off, the error message is confusing, mentioning the mysterious `<>`. But more importantly, it would be nice if the `Typeable` mechanism supported coercions.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14119Refactor type patterns20190707T18:18:23ZRichard Eisenbergrae@richarde.devRefactor type patternsType patterns are used in instance heads: class instances, type instances, and data/newtype instances. These type patterns differ from ordinary types in several ways:
 They must never mention a `forall`.
 They must never mention a con...Type patterns are used in instance heads: class instances, type instances, and data/newtype instances. These type patterns differ from ordinary types in several ways:
 They must never mention a `forall`.
 They must never mention a context. (The context in a class instance head is a different part of the instance construct.)
 They must never mention a type family.
Types that appear as arguments on the LHS of a RULE should also be type patterns.
Type patterns are used in GHC differently than types as well: we should match only against patterns, never ordinary types.
I thus propose that a new datatype within GHC to store type patterns. I'll call it `TyPat` here, but perhaps a longer name is better. The matcher (in the `Unify` module) would then take a `TyPat` parameter, making clear which type is the template and which is the concrete instantiation.
We could have a new algorithm to typecheck/desugar source syntax into patterns. This new algorithm could accommodate issues like those mentioned in [ticket:14038\#comment:140786](https://gitlab.haskell.org//ghc/ghc/issues/14038#note_140786). It could also avoid ever putting a type family in a kind parameter, which would fix #12564. Separating out checking type patterns from proper types could also improve GADT pattern matching in types, which is currently more like "wobbly types" than OutsideIn.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Task 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  #12564, #14038 
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Refactor type patterns","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"Type patterns are used in instance heads: class instances, type instances, and data/newtype instances. These type patterns differ from ordinary types in several ways:\r\n\r\n * They must never mention a `forall`.\r\n * They must never mention a context. (The context in a class instance head is a different part of the instance construct.)\r\n * They must never mention a type family.\r\n\r\nTypes that appear as arguments on the LHS of a RULE should also be type patterns.\r\n\r\nType patterns are used in GHC differently than types as well: we should match only against patterns, never ordinary types.\r\n\r\nI thus propose that a new datatype within GHC to store type patterns. I'll call it `TyPat` here, but perhaps a longer name is better. The matcher (in the `Unify` module) would then take a `TyPat` parameter, making clear which type is the template and which is the concrete instantiation.\r\n\r\nWe could have a new algorithm to typecheck/desugar source syntax into patterns. This new algorithm could accommodate issues like those mentioned in comment:6:ticket:14038. It could also avoid ever putting a type family in a kind parameter, which would fix #12564. Separating out checking type patterns from proper types could also improve GADT pattern matching in types, which is currently more like \"wobbly types\" than OutsideIn.","type_of_failure":"OtherFailure","blocking":[12564,14038]} >Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/15588Panic when abusing kind inference20190707T18:04:01ZRichard Eisenbergrae@richarde.devPanic when abusing kind inferenceWhen I say
```hs
{# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,
AllowAmbiguousTypes #}
import Data.Proxy
import Data.Type.Equality
import Data.Type.Bool
import Data.Kind
data SameKind :: foral...When I say
```hs
{# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,
AllowAmbiguousTypes #}
import Data.Proxy
import Data.Type.Equality
import Data.Type.Bool
import Data.Kind
data SameKind :: forall k. k > k > Type
type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where
IfK (_ :: Proxy True) f _ = f
IfK (_ :: Proxy False) _ g = g
y :: forall ck (c :: ck). ck :~: Proxy True > ()
y Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d
x = undefined
in ()
```
HEAD says
```
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.7.20180827 for x86_64appledarwin):
ASSERT failed!
Bad coercion hole co_a3iZ: If
j_a3j0[tau:2] m_a3j1[tau:2] a_a3gV[sk:3]
a_a3gV[sk:3]
nominal
If j_a3j0[tau:2] m_a3j1[tau:2] a_a3jj[sk:3] ~# a_a3jj[sk:3]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable
assertPprPanic, called at compiler/typecheck/TcMType.hs:316:25 in ghc:TcMType
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
It's as yet unclear whether the program should be accepted. My best guess is that it should, but that (even with this panic fixed) GHC isn't up to the task.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 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":"Panic when abusing kind inference","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When I say\r\n\r\n{{{#!hs\r\n{# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,\r\n AllowAmbiguousTypes #}\r\n\r\nimport Data.Proxy\r\nimport Data.Type.Equality\r\nimport Data.Type.Bool\r\nimport Data.Kind\r\n\r\ndata SameKind :: forall k. k > k > Type\r\ntype family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where\r\n IfK (_ :: Proxy True) f _ = f\r\n IfK (_ :: Proxy False) _ g = g\r\n\r\ny :: forall ck (c :: ck). ck :~: Proxy True > ()\r\ny Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d\r\n x = undefined\r\n in ()\r\n}}}\r\n\r\nHEAD says\r\n\r\n{{{\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20180827 for x86_64appledarwin):\r\n\tASSERT failed!\r\n Bad coercion hole co_a3iZ: If\r\n j_a3j0[tau:2] m_a3j1[tau:2] a_a3gV[sk:3]\r\n a_a3gV[sk:3]\r\n nominal\r\n If j_a3j0[tau:2] m_a3j1[tau:2] a_a3jj[sk:3] ~# a_a3jj[sk:3]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable\r\n assertPprPanic, called at compiler/typecheck/TcMType.hs:316:25 in ghc:TcMType\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\n\r\nIt's as yet unclear whether the program should be accepted. My best guess is that it should, but that (even with this panic fixed) GHC isn't up to the task.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15589Always promoting metavariables during type inference may be wrong20190707T18:04:00ZRichard Eisenbergrae@richarde.devAlways promoting metavariables during type inference may be wrongCurrently, when checking a type signature, GHC promotes all the metavariables that arise during checking as soon as it's done checking the signature. This may be incorrect sometimes.
Consider
```hs
{# LANGUAGE ScopedTypeVariables, Typ...Currently, when checking a type signature, GHC promotes all the metavariables that arise during checking as soon as it's done checking the signature. This may be incorrect sometimes.
Consider
```hs
{# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,
AllowAmbiguousTypes #}
import Data.Proxy
import Data.Type.Equality
import Data.Type.Bool
import Data.Kind
data SameKind :: forall k. k > k > Type
type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where
IfK (_ :: Proxy True) f _ = f
IfK (_ :: Proxy False) _ g = g
y :: forall (cb :: Bool) (c :: Proxy cb). cb :~: True > ()
y Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d
x = undefined
in ()
```
This panics currently (#15588), but I'm pretty sure it will erroneously be rejected even after the panic is fixed. Let's walk through it.
 We can derive `IfK :: forall (j :: Bool) (m :: Type) (n :: Type). Proxy j > m > n > If j m n`, where `If :: forall k. Bool > k > k > k` is imported from `Data.Type.Bool` and is a straightforward conditional choice operator.
 In the type of `x`, we see that we need the kind of `IfK c b d` to match the kind of `d`. That is, if `b :: kappa[3]`, we have `[W] If cb kappa[3] a ~ a`. Here, the `forall` in `x`'s type is at level 3; the RHS of `y` is at level 2.
 If we could reduce `If cb kappa[3] a` to `kappa[3]`, then we would solve `kappa[3] := a`, but we can't make this reduction, because `cb` is a skolem.
 Instead, we finish checking the type of `x` and promote `kappa[3]` to `kappa[2]`.
 Later, we'll make an implication constraint with `[G] cb ~ True`. When solving that implication constraint, we'll get `[W] If True kappa[2] a ~ a` and simplify to `[W] kappa[2] ~ a`, but that will be insoluble because we'll be solving at level 3, and now `kappa[2]` is at level 2. We're too late.
Yet, I claim that this program should be accepted, and it would be if GHC tracked a set of ambient givens and used them in local calls to the solver. With these "ambient givens" (instead of putting them only in implication constraints), we would know `cb ~ True` the first time we try to solve, and then we'll succeed.
An alternative story is to change how levels are used with variables. Currently, levels are, essentially, the number of type variables available from an outer scope. Accordingly, we must make sure that the level of a variable is never higher than the ambient level. (If it were, we wouldn't know what extra variable(s) were in scope.) Instead, we could just store the list of variables that were in scope. We wouldn't then need to promote in this case  promotion would happen only during floating. But tracking these lists is a real pain. (If we decide to pursue this further, I can add more details, but it's all in Chapter 6 in [my thesis](https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1074&context=compsci_pubs)  section 6.5 to be specific.)
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 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":"Always promoting metavariables during type inference may be wrong","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Currently, when checking a type signature, GHC promotes all the metavariables that arise during checking as soon as it's done checking the signature. This may be incorrect sometimes.\r\n\r\nConsider\r\n\r\n{{{#!hs\r\n{# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,\r\n AllowAmbiguousTypes #}\r\n\r\nimport Data.Proxy\r\nimport Data.Type.Equality\r\nimport Data.Type.Bool\r\nimport Data.Kind\r\n\r\ndata SameKind :: forall k. k > k > Type\r\ntype family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where\r\n IfK (_ :: Proxy True) f _ = f\r\n IfK (_ :: Proxy False) _ g = g\r\n\r\ny :: forall (cb :: Bool) (c :: Proxy cb). cb :~: True > ()\r\ny Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d\r\n x = undefined\r\n in ()\r\n}}}\r\n\r\nThis panics currently (#15588), but I'm pretty sure it will erroneously be rejected even after the panic is fixed. Let's walk through it.\r\n\r\n* We can derive `IfK :: forall (j :: Bool) (m :: Type) (n :: Type). Proxy j > m > n > If j m n`, where `If :: forall k. Bool > k > k > k` is imported from `Data.Type.Bool` and is a straightforward conditional choice operator.\r\n\r\n* In the type of `x`, we see that we need the kind of `IfK c b d` to match the kind of `d`. That is, if `b :: kappa[3]`, we have `[W] If cb kappa[3] a ~ a`. Here, the `forall` in `x`'s type is at level 3; the RHS of `y` is at level 2.\r\n\r\n* If we could reduce `If cb kappa[3] a` to `kappa[3]`, then we would solve `kappa[3] := a`, but we can't make this reduction, because `cb` is a skolem.\r\n\r\n* Instead, we finish checking the type of `x` and promote `kappa[3]` to `kappa[2]`.\r\n\r\n* Later, we'll make an implication constraint with `[G] cb ~ True`. When solving that implication constraint, we'll get `[W] If True kappa[2] a ~ a` and simplify to `[W] kappa[2] ~ a`, but that will be insoluble because we'll be solving at level 3, and now `kappa[2]` is at level 2. We're too late.\r\n\r\nYet, I claim that this program should be accepted, and it would be if GHC tracked a set of ambient givens and used them in local calls to the solver. With these \"ambient givens\" (instead of putting them only in implication constraints), we would know `cb ~ True` the first time we try to solve, and then we'll succeed.\r\n\r\nAn alternative story is to change how levels are used with variables. Currently, levels are, essentially, the number of type variables available from an outer scope. Accordingly, we must make sure that the level of a variable is never higher than the ambient level. (If it were, we wouldn't know what extra variable(s) were in scope.) Instead, we could just store the list of variables that were in scope. We wouldn't then need to promote in this case  promotion would happen only during floating. But tracking these lists is a real pain. (If we decide to pursue this further, I can add more details, but it's all in Chapter 6 in [https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1074&context=compsci_pubs my thesis]  section 6.5 to be specific.)","type_of_failure":"OtherFailure","blocking":[]} >8.6.1