GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2022-01-25T21:49:09Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/14420Data families should not instantiate to non-Type kinds2022-01-25T21:49:09ZRichard Eisenbergrae@richarde.devData families should not instantiate to non-Type kinds```hs
data family Any :: k -- allowable now due to fix for #12369
type family F (a :: Bool) :: Nat where
F True = 0
F False = 1
F Any = 2
```
```
ghci> :kind! F True
F True :: Nat
= 0
ghci> :kind! F False
F False :: Nat
= 1
g...```hs
data family Any :: k -- allowable now due to fix for #12369
type family F (a :: Bool) :: Nat where
F True = 0
F False = 1
F Any = 2
```
```
ghci> :kind! F True
F True :: Nat
= 0
ghci> :kind! F False
F False :: Nat
= 1
ghci> :kind! F Any
F Any :: Nat
= 2
```
Oh dear.
We should require that any instantiation of a data family be to a kind that ends in `Type`.
Inspired by [ticket:9429\#comment:144757](https://gitlab.haskell.org//ghc/ghc/issues/9429#note_144757)
<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":"Data families should not instantiate to non-Type kinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\ndata family Any :: k -- allowable now due to fix for #12369\r\n\r\ntype family F (a :: Bool) :: Nat where\r\n F True = 0\r\n F False = 1\r\n F Any = 2\r\n}}}\r\n\r\n{{{\r\nghci> :kind! F True\r\nF True :: Nat\r\n= 0\r\nghci> :kind! F False\r\nF False :: Nat\r\n= 1\r\nghci> :kind! F Any\r\nF Any :: Nat\r\n= 2\r\n}}}\r\n\r\nOh dear.\r\n\r\nWe should require that any instantiation of a data family be to a kind that ends in `Type`.\r\n\r\nInspired by comment:31:ticket:9429","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/17567Never `Any`-ify during kind inference2021-01-11T13:09:30ZRichard Eisenbergrae@richarde.devNever `Any`-ify during kind inference#14198 concludes with a new plan: never `Any`-ify during kind inference. This ticket tracks this particular problem, separate from #14198.
Here are some examples of `Any`-ification during kind inference:
#17301:
```hs
data B a
...#14198 concludes with a new plan: never `Any`-ify during kind inference. This ticket tracks this particular problem, separate from #14198.
Here are some examples of `Any`-ification during kind inference:
#17301:
```hs
data B a
data TySing ty where
SB :: TySing (B a)
data ATySing where
MkATySing :: TySing ty -> ATySing
type family Forget ty :: ATySing where
Forget (B a) = MkATySing SB
```
The RHS of that type family equation is really `MkATySing @alpha (SB @alpha)`, and the `alpha` gets zonked to `Any`.
#14198:
```hs
type T = forall a. Proxy a
```
The RHS of the type synonym is really `forall (a :: kappa). Proxy @kappa a`, and the `kappa` gets zonked to `Any`.
#17562:
```hs
class (forall a. a b ~ a c) => C b c
```
The superclass constraint is really `forall (a :: Type -> kappa). (~) @kappa (a b) (a c))`, and the `kappa` gets zonked to `Any`.
We want to stop zonking to `Any`, preferring to error instead. But how should we implement?
* Option A: Use a new variant of `ZonkFlexi`, a choice carried around in a `ZonkEnv` that says what to do with empty metavariables. The new choice would cause an error. This new form of `ZonkFlexi` would be used in the final zonks in e.g. TcTyClsDecls. Open question: how to get a decent error message? I think we'd have to pass around the original, top-level type in order to report it. By the time we have just the unbound metavariable, we have no context to report.
* Option B: Similar to (A), but don't report an error in the zonker. Instead, the new variant of `ZonkFlexi` would insert some magical error type. Then, the validity checker could do an early pass, looking for the error type; it can then report a nice error message.
* Option C: Look for all cases where `Any`-ification might happen, and detect each one separately. This can produce lovely error messages. The solution for #17562 in !2313 does this. Perhaps we can pair this choice with a new `ZonkFlexi` that panics. That way, we'll know if we've missed a case.
* Simon below proposes Option D: Zap to `Type` instead of `Any`. I (Richard) view D as an add-on to any of the above plans. Because `Type` is not always well-kinded, we can only zap to `Type` sometimes, and we still need to decide what we do at other times. Personally, I prefer not to treat `Type` specially with -XPolyKinds` enabled, and so I'd prefer that we don't do this.
* EDIT: Also, we can consider Option E: Report poor error messages, saying something about an unconstrained kind variable. Users would be helped only via the context (the "In the data declaration for `Wurble`" bits). This would mean building up useful contexts in the zonker.
* Option F: The new constructor for `ZonkFlexi` could carry the top-level type we are trying to zonk. If we encounter an unconstrained metavariable, we just look at this bit of context to produce the error message. Perhaps this could be combined with the context-building in Option E for good effect. This is the first solution I'm actually happy with.
Thoughts?https://gitlab.haskell.org/ghc/ghc/-/issues/12612Allow kinds of associated types to depend on earlier associated types2023-12-22T08:53:22ZdavemenendezAllow 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 [e-mail discussion](https://mail.haskell.org/pipermail/glasgow-haskell-users/2016-September/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/glasgow-haskell-users/2016-September/026402.html e-mail 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/20356Constraint-vs-Type causes a panic2021-10-22T17:00:34ZRichard Eisenbergrae@richarde.devConstraint-vs-Type causes a panic@monoidal observes in https://gitlab.haskell.org/ghc/ghc/-/issues/11715#note_375240 that
```hs
{-# LANGUAGE TypeFamilies, PolyKinds, ConstraintKinds #-}
import GHC.Types
type family Id (a :: k -> Constraint) :: l -> Constraint
type inst...@monoidal observes in https://gitlab.haskell.org/ghc/ghc/-/issues/11715#note_375240 that
```hs
{-# LANGUAGE TypeFamilies, PolyKinds, ConstraintKinds #-}
import GHC.Types
type family Id (a :: k -> Constraint) :: l -> Constraint
type instance Id f = f
type T :: Constraint -> Constraint
type T = Id Eq
data Proxy p = MkProxy
id' :: f a -> f a
id' x = x
z = id' (MkProxy @T)
```
causes
```
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.3.20210824:
ASSERT failed!
Ill-kinded update to meta tyvar
a_aIJ[tau:1] :: Constraint -> Constraint
Constraint -> Constraint := Eq :: * -> Constraint
Call stack:
CallStack (from HasCallStack):
massertPpr, called at compiler/GHC/Tc/Utils/TcMType.hs:1009:10 in ghc:GHC.Tc.Utils.TcMType
```
when assertions are enabled (e.g. a `DEBUG` compiler).
Constraint-vs-Type is a difficult problem (see #11715), but I think we can pull this off and fix it. I imagine we just need to change an `eqType` to `tcEqType` somewhere.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/20312Deprecate -XTypeInType2022-06-06T16:13:20ZKrzysztof GogolewskiDeprecate -XTypeInTypeAccording to the accepted proposal [Embrace (Type :: Type)](https://github.com/ghc-proposals/ghc-proposals/pull/83)
> Two releases after this proposal is implemented, deprecate -XTypeInType.
The proposal has been implemented in GHC 8.6...According to the accepted proposal [Embrace (Type :: Type)](https://github.com/ghc-proposals/ghc-proposals/pull/83)
> Two releases after this proposal is implemented, deprecate -XTypeInType.
The proposal has been implemented in GHC 8.6. We can now deprecate `-XTypeInType`. The deprecation message should mention that it is replaced by `DataKinds` + `PolyKinds`.Rinat Striungislazybonesxp@gmail.comRinat Striungislazybonesxp@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/20172Coercion prevents type family equation from applying2021-07-27T21:31:47ZRichard Eisenbergrae@richarde.devCoercion prevents type family equation from applyingGHC rejects this program:
```hs
{-# LANGUAGE ExplicitForAll, PolyKinds, StandaloneKindSignatures,
TypeFamilies, DataKinds #-}
module Bug where
import Data.Kind
type F :: Type -> Type
type family F k where
F k = Type
t...GHC rejects this program:
```hs
{-# LANGUAGE ExplicitForAll, PolyKinds, StandaloneKindSignatures,
TypeFamilies, DataKinds #-}
module Bug where
import Data.Kind
type F :: Type -> Type
type family F k where
F k = Type
type family G a where
forall (k :: Type) (a :: Type -> F k) (b :: Type). G (a b, k) = Char
x :: G (Maybe Int, Bool)
x = 'y'
```
It would be accepted if the `a` were missing its kind signature in the equation for `G`.
The problem is that we end up with a template like `((a b) |> co, k)` , and GHC's matcher does not know how to propagate a coercion that casts the result of an application.
Closely related to #20146, #20171https://gitlab.haskell.org/ghc/ghc/-/issues/20171Core Lint error around pure unifier and coercions2023-05-16T20:10:31ZRichard Eisenbergrae@richarde.devCore Lint error around pure unifier and coercionsThis ticket is closely related to #20146, #20172
If I say
```hs
{-# LANGUAGE ExplicitForAll, PolyKinds, StandaloneKindSignatures,
TypeFamilies, DataKinds #-}
module Bug where
import Data.Kind
type F :: Type -> Type
typ...This ticket is closely related to #20146, #20172
If I say
```hs
{-# LANGUAGE ExplicitForAll, PolyKinds, StandaloneKindSignatures,
TypeFamilies, DataKinds #-}
module Bug where
import Data.Kind
type F :: Type -> Type
type family F k where
F k = Type -> Type
type family G a where
forall (k :: Type) (a :: F k) (b :: Type). G (a b, k) = Char
x :: G (Maybe Int, Bool)
x = 'y'
```
I get (with `-dcore-lint`)
```
*** Core Lint errors : in result of Desugar (before optimization) ***
Bug.hs:16:1: warning:
The type variable @k_auc is out of scope
In the RHS of x :: G (Maybe Int, Bool)
Substitution: [TCvSubst
In scope: InScope {}
Type env: []
Co env: []]
*** Offending Program ***
Rec {
$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "Bug"#)
x :: G (Maybe Int, Bool)
[LclIdX]
x = (C# 'y'#)
`cast` (Sub (Sym (D:R:G[0]
<Bool>_N <(Maybe |> Sym (D:R:F[0] <k_auc>_N))>_N <Int>_N))
:: Char ~R# G (Maybe Int, Bool))
end Rec }
*** End of Offense ***
```
The problem is the `kco` parameter in the pure unifier.
When we have target: `ty1 |> co` and template: `ty2`, GHC remembers `co` as the relationship between the kinds of `ty1` and `ty2`, and then matches `ty1` against `ty2`. The problem is that this "remembered coercion" (called `kco` in the code) sometimes comes from the template (as here) and sometimes from the target. It thus mixes variables from both the template and the target.
This is addressed in Note [Matching in the presence of casts (1)] in GHC.Core.Unify. However, that Note is subtly wrong, in the presence of a type like `(a |> co) b`, which is what we have here. Specifically, we have
template variables: `k :: Type`, `a :: F k`, `b :: Type`
template: `((a |> axF[k]) b, k)`
target: `(Maybe Int, Bool)`
where `axF :: [k]. F k ~ (Type -> Type)`. (The `[k]` notation says that `k` is a parameter of the axiom.)
The matcher goes left-to-right, and thus matches `a |-> Maybe |> sym axF[k]` *before* it matches `k`. The `k` thus ends up in the final substitution, free.
Possible solutions:
1. Require the `kco` to mention only variables from the target, never the template (as today). Then, whenever the matcher sees a coercion in the template (e.g. `ty |> co`), create a fresh variable `cv` and remember the coercion spotted in the template (e.g. `co`). At the end, apply the substitution that is the result of the (successful) match to the remembered coercions, and then build a substitution mapping the fresh `cv`s to the substituted remembered `co`s. This would work, but it would perhaps need to run this process several times. Essentially, this is all about propagating the information about `k` back to an earlier point in the match.
2. Require the template and the target to have distinct sets of free variables. Then, we don't have to worry about mixing them together. At the end of a successful match, just find the fixpoint of the substitution. (This fixpoint operation already happens for two-way unification -- not one-way matching -- which is done by the same body of code. This approach might thus simplify some of the mediating between matching and unification already present.) We could choose to skip the fixpoint calculation if no coercions were encountered in the template, the vastly common case.
3. Forbid type families in the kinds of template variables (much like type families are generally forbidden in templates). Since we have no free coercion variables in templates and no type families in them either, it would seem that all coercions must be reflexive, thus sidestepping the problem. This seems delicate though, and likely not to be true forever (example: `unsafeCoerce` in types).
Right now, (2) seems most appealing.https://gitlab.haskell.org/ghc/ghc/-/issues/19802Pure unifier is incomplete around casts and AppTys: instance lookup fails2021-05-10T10:15:47ZRichard Eisenbergrae@richarde.devPure unifier is incomplete around casts and AppTys: instance lookup failsThe pure unifier (in `GHC.Core.Unify`) is incomplete with respect to casts. Here is the counter-example:
```
alpha :: Type -> Type -- this is the template variable
a :: Type -> k
co :: k ~ Type
(alpha Int) ~? (a Int |> co)
...The pure unifier (in `GHC.Core.Unify`) is incomplete with respect to casts. Here is the counter-example:
```
alpha :: Type -> Type -- this is the template variable
a :: Type -> k
co :: k ~ Type
(alpha Int) ~? (a Int |> co)
```
Today, the pure unifier will claim that these two types have no unifier. But they do:
```
alpha :-> a |> <Type> -> co
```
This, unfortunately, will not be easy to solve. We will have to somehow remember the casts that we see as we descend into a type, and use those casts for rewriting.
Here is a concrete program that witnesses the problem:
```hs
{-# LANGUAGE FlexibleInstances, TypeFamilies, ExplicitForAll, KindSignatures,
DataKinds #-}
module Bug where
import Data.Kind ( Type )
class C a where
meth :: a -> ()
instance C (b Int) where
meth _ = ()
type family Star where
Star = Type
f :: forall (c :: Type -> Star). c Int -> ()
f x = meth x
```
As written, it fails with
```
Bug.hs:17:7: error:
• No instance for (C (c Int)) arising from a use of ‘meth’
• In the expression: meth x
In an equation for ‘f’: f x = meth x
|
17 | f x = meth x
| ^^^^^^
```
But change the type of `c` to become `Type -> Type`, and the program is accepted.https://gitlab.haskell.org/ghc/ghc/-/issues/19677GHC does not rewrite in FunTy2022-02-21T17:09:27ZRichard Eisenbergrae@richarde.devGHC does not rewrite in FunTyConsider
```hs
{-# LANGUAGE ExplicitForAll, PolyKinds, DataKinds, TypeFamilies, GADTs #-}
module Bug where
import GHC.Exts
class C x where
meth :: x -> ()
instance C (a -> b) where
meth _ = ()
type family Lifty throttle where
...Consider
```hs
{-# LANGUAGE ExplicitForAll, PolyKinds, DataKinds, TypeFamilies, GADTs #-}
module Bug where
import GHC.Exts
class C x where
meth :: x -> ()
instance C (a -> b) where
meth _ = ()
type family Lifty throttle where
Lifty Int = LiftedRep
data G a where
MkG :: G Int
foo :: forall i (a :: TYPE (Lifty i)) (b :: TYPE (Lifty i)). G i -> (a -> b) -> ()
foo MkG = meth
```
GHC rejects, saying it cannot find an instance for `C (a -> b)`. But it should accept.
The problem is that the kinds of `a` and `b` are `TYPE (Lifty i)`. Even if we know `i ~ Int`, and therefore that `Lifty i ~ LiftedRep`, GHC does not rewrite these kinds internally, allowing instance matching to succeed.
!2477, when complete, should address this.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/19652GHC's failure to rewrite in coercions & kinds leads to spurious occurs-check ...2021-04-08T08:48:53ZRichard Eisenbergrae@richarde.devGHC's failure to rewrite in coercions & kinds leads to spurious occurs-check failureConsider this mess:
```hs
{-# LANGUAGE ExplicitForAll, PolyKinds, DataKinds, TypeFamilies,
StandaloneKindSignatures, AllowAmbiguousTypes, GADTs,
TypeOperators #-}
module Bug where
import Data.Kind ( Type )
im...Consider this mess:
```hs
{-# LANGUAGE ExplicitForAll, PolyKinds, DataKinds, TypeFamilies,
StandaloneKindSignatures, AllowAmbiguousTypes, GADTs,
TypeOperators #-}
module Bug where
import Data.Kind ( Type )
import Data.Type.Equality ( type (~~) )
import Data.Proxy ( Proxy )
type Const :: () -> k1 -> k2 -> k1
type family Const u x y where
Const '() x y = x
type Equals :: k1 -> k2 -> Type
type family Equals a b where
Equals a a = Char
Equals a b = Bool
type IsUnit :: () -> Type
data IsUnit u where
ItIs :: IsUnit '()
f :: forall (u :: ()) (a :: Type) (b :: Const u Type a). (a ~~ b)
=> IsUnit u -> a -> Proxy b -> Equals a b
f ItIs _ _ = 'x'
g = f ItIs
```
GHC fails (in the RHS of `g`) with an occurs-check, but it should succeed.
The problem is that we end up with
```
[W] (alpha :: Type) ~# (beta :: Const upsilon Type alpha)
```
where we have already unified `upsilon := '()`.
But GHC refuses to rewrite in kinds, so the `Const` never reduces, and we reject the program. Note that a solution exists, with `alpha := Any @Type` and `beta := Any @Type |> sym (AxConst Type (Any @Type))`.
Proposed solution:
The wanted above actually gets simplified to become
```
[W] co :: Const '() Type alpha ~# Type
[W] w2 :: (alpha :: Type) ~# ((beta |> co) :: Type)
```
The `co` is easily solved. Then, when we get to `w2`, we are in Wrinkle (3) of Note [Equalities with incompatible kinds]. Happily, we should be able to detect that `alpha` is free in `co` and reorient, giving
```
[W] w3 :: (beta :: Const '() Type alpha) ~# (alpha |> sym co :: Const '() Type alpha)
```
which can be solved by unifying `beta := alpha |> sym co`. `alpha` will then remain unconstrained and will be zonked to `Any`.
The key new part is looking at the coercion when deciding whether to reorient.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/19196TypeInType prevents Typeable from being resolved from a given2021-01-11T03:19:52ZSerge KosyrevTypeInType prevents Typeable from being resolved from a givenThe following program is accepted without `TypeInType` by GHC 8.10.2:
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}...The following program is accepted without `TypeInType` by GHC 8.10.2:
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Dynamic
import Type.Reflection
data Liveness
= forall t. Live t
data IOA (l :: Liveness) where
IOE :: IOA (Live t)
data LTag (l :: Liveness) where
LLive :: Typeable t => TypeRep t -> LTag (Live t)
reconstruct :: Dynamic -> LTag l -> ()
reconstruct dyn l@LLive{} =
case l of
(LLive tr :: LTag (Live t)) ->
undefined $ withTypeable tr $
(fromDynamic dyn :: Maybe (IOA (Live t)))
main :: IO ()
main = undefined
```
It is, however, rejected with `TypeInType`, as follows:
```haskell
common/src/Dom/Pipe/IOA.hs:26:17: error:
• Could not deduce (Typeable t) arising from a use of ‘fromDynamic’
from the context: (l ~ 'Live t1, Typeable t1)
bound by a pattern with constructor:
LLive :: forall t1 (t2 :: t1).
Typeable t2 =>
TypeRep t2 -> LTag ('Live t2),
in an equation for ‘reconstruct’
at common/src/Dom/Pipe/IOA.hs:22:19-25
or from: ('Live t1 ~ 'Live t3, Typeable t3)
bound by a pattern with constructor:
LLive :: forall t1 (t2 :: t1).
Typeable t2 =>
TypeRep t2 -> LTag ('Live t2),
in a case alternative
at common/src/Dom/Pipe/IOA.hs:24:10-17
or from: Typeable t3
bound by a type expected by the context:
Typeable t3 => Maybe (IOA ('Live t1))
at common/src/Dom/Pipe/IOA.hs:26:16-56
• In the second argument of ‘($)’, namely
‘(fromDynamic dyn :: Maybe (IOA (Live t)))’
In the second argument of ‘($)’, namely
‘withTypeable tr $ (fromDynamic dyn :: Maybe (IOA (Live t)))’
In the expression:
undefined
$ withTypeable tr $ (fromDynamic dyn :: Maybe (IOA (Live t)))
|
26 | (fromDynamic dyn :: Maybe (IOA (Live t)))
| ^^^^^^^^^^^^^^^
```
Potentially related to #16627https://gitlab.haskell.org/ghc/ghc/-/issues/18891Kind inference for newtypes in GADT syntax is deeply broken2020-12-08T21:03:16ZRichard Eisenbergrae@richarde.devKind inference for newtypes in GADT syntax is deeply brokenHere are some tales of destruction, all with `-XUnliftedNewtypes` and `-XNoCUSKs`:
```hs
newtype N :: forall k. TYPE k where
MkN :: N -> N
```
gives
```
Scratch.hs:34:3: error:
• Expected a type, but ‘N’ has kind ‘*’
• In th...Here are some tales of destruction, all with `-XUnliftedNewtypes` and `-XNoCUSKs`:
```hs
newtype N :: forall k. TYPE k where
MkN :: N -> N
```
gives
```
Scratch.hs:34:3: error:
• Expected a type, but ‘N’ has kind ‘*’
• In the definition of data constructor ‘MkN’
In the newtype declaration for ‘N’
```
------------------------
```hs
type N :: forall k. TYPE k
newtype N :: forall k. TYPE k where
MkN :: N -> N
```
gives
```
Scratch.hs:35:3: error:
• A newtype constructor must have a return type of form T a1 ... an
MkN :: N -> N
• In the definition of data constructor ‘MkN’
In the newtype declaration for ‘N’
```
-------------------------
```hs
newtype N :: forall k -> TYPE k where
MkN :: N m -> N m
```
gives
```
Scratch.hs:35:3: error:
• Expected a type, but ‘N m’ has kind ‘TYPE m’
• In the definition of data constructor ‘MkN’
In the newtype declaration for ‘N’
```
-------------------------
```hs
type N :: forall k -> TYPE k
newtype N :: forall k -> TYPE k where
MkN :: N m -> N m
```
succeeds.
I think all these examples should succeed. All but the last cause a DEBUG build of GHC to panic.
I think the problem is that the `res_kind` passed to `kcConArgTys` has the wrong scope: it mentions variables in the type head, but these are utterly distinct from the variables in the constructor type.9.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/18753Tighten up the treatment of loose types in the solver2020-09-30T16:21:20ZRichard Eisenbergrae@richarde.devTighten up the treatment of loose types in the solver`GHC.Tc.Solver.Monad` includes
```
Note [Use loose types in inert set]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Say we know (Eq (a |> c1)) and we need (Eq (a |> c2)). One is clearly
solvable from the other. So, we do lookup in the inert set...`GHC.Tc.Solver.Monad` includes
```
Note [Use loose types in inert set]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Say we know (Eq (a |> c1)) and we need (Eq (a |> c2)). One is clearly
solvable from the other. So, we do lookup in the inert set using
loose types, which omits the kind-check.
We must be careful when using the result of a lookup because it may
not match the requested info exactly!
```
There are several problems.
* We aren't always careful. For example, `lookupInInerts` tries `lookupSolvedDict` and then `lookupInertDict`, both of which use this "loose" lookup. Yet the result of `lookupInInerts` just uses the result, without any special handling to take the fact that the types might not match exactly.
* The Note doesn't actually make sense. The only difference between `Eq (a |> c1)` and `Eq (a |> c2)` is the coercion. But I sincerely hope we never care about the contents of a coercion. So even if we use evidence of type `Eq (a |> c1)` where GHC is expecting `Eq (a |> c2)` (assuming `c1` and `c2` have the same type), all will be well.
* What I think the Note is trying to say will never happen. That is, the actual implementation of the inert-set lookup tries to match types while ignoring their kinds. (Normal type matching requires that the kind matches also.) So a better example would be something like comparing `Eq (a :: k1)` with `Eq (a :: k2)`. But that's impossible, even with casts: all type families and classes have *closed* kinds, meaning that any variables that appear in the kinds of arguments must themselves be earlier arguments. In other words, if I have well-typed `T blah1 (... :: kind1)` and `T blah2 (... :: kind2)`, then either `kind1` equals `kind2` or `blah1` and `blah2` must differ. We use this logic elsewhere -- in particular, in the pure unifier.
Conclusions:
* Using "loose" matching (that is, ignoring kinds) in the solver is the right thing.
* We should update the Note with my argument above.
* No special care needs to be taken when using loose matching in this way. This means we can drop a few redundant equality checks (e.g. in `lookupFlatCache`).
I'm pretty confident about this all, but I'd like a double-check before I commit a fix.https://gitlab.haskell.org/ghc/ghc/-/issues/18714GHC panic (tcInvisibleTyBinder) when using constraint in a kind2020-09-21T21:17:06ZRyan ScottGHC panic (tcInvisibleTyBinder) when using constraint in a kindThe following program will panic when compiled with GHC 8.10 or HEAD:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
module Bug where
import GHC.Exts
type Id...The following program will panic when compiled with GHC 8.10 or HEAD:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
module Bug where
import GHC.Exts
type Id a = a
type F = Id (Any :: forall a. Show a => a -> a)
```
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.10.2:
tcInvisibleTyBinder
Show a_avp[sk:2]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1179:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/Inst.hs:460:5 in ghc:Inst
```
I'm a bit surprised that this happens, since GHC has a validity check intended to rule out the use of arbitrary constraints in kinds. This check is implemented by [`GHC.Tc.Validity.allConstraintsAllowed`](https://gitlab.haskell.org/ghc/ghc/-/blob/a1f34d37b47826e86343e368a5c00f1a4b1f2bce/compiler/GHC/Tc/Validity.hs#L473-480):
```hs
allConstraintsAllowed :: UserTypeCtxt -> Bool
-- We don't allow arbitrary constraints in kinds
allConstraintsAllowed (TyVarBndrKindCtxt {}) = False
allConstraintsAllowed (DataKindCtxt {}) = False
allConstraintsAllowed (TySynKindCtxt {}) = False
allConstraintsAllowed (TyFamResKindCtxt {}) = False
allConstraintsAllowed (StandaloneKindSigCtxt {}) = False
allConstraintsAllowed _ = True
```
Upon closer inspection, `allConstraintsAllowed` appears to be incomplete. Compare this to [`GHC.Tc.Validity.vdqAllowed`](https://gitlab.haskell.org/ghc/ghc/-/blob/a1f34d37b47826e86343e368a5c00f1a4b1f2bce/compiler/GHC/Tc/Validity.hs#L496-507), which must also make a distinction between types and kinds:
```hs
vdqAllowed :: UserTypeCtxt -> Bool
-- Currently allowed in the kinds of types...
vdqAllowed (KindSigCtxt {}) = True
vdqAllowed (StandaloneKindSigCtxt {}) = True
vdqAllowed (TySynCtxt {}) = True
vdqAllowed (ThBrackCtxt {}) = True
vdqAllowed (GhciCtxt {}) = True
vdqAllowed (TyVarBndrKindCtxt {}) = True
vdqAllowed (DataKindCtxt {}) = True
vdqAllowed (TySynKindCtxt {}) = True
vdqAllowed (TyFamResKindCtxt {}) = True
-- ...but not in the types of terms.
...
```
Note that `vdqAllowed` identifies more `UserTypeCtxt`s as being kind-level positions than `allConstraintsAllowed` does. Crucially, `allConstraintsAllowed` omits a case for `KindSigCtxt`. If I add such as case:
```diff
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index fba45562b7..39ebc260da 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -479,6 +479,7 @@ allConstraintsAllowed (DataKindCtxt {}) = False
allConstraintsAllowed (TySynKindCtxt {}) = False
allConstraintsAllowed (TyFamResKindCtxt {}) = False
allConstraintsAllowed (StandaloneKindSigCtxt {}) = False
+allConstraintsAllowed (KindSigCtxt {}) = False
allConstraintsAllowed _ = True
-- | Returns 'True' if the supplied 'UserTypeCtxt' is unambiguously not the
```
Then the program above no longer panics:
```
$ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:14: error:
• Illegal constraint in a kind: forall a. Show a => a -> a
• In the first argument of ‘Id’, namely
‘(Any :: forall a. Show a => a -> a)’
In the type ‘Id (Any :: forall a. Show a => a -> a)’
In the type declaration for ‘F’
|
11 | type F = Id (Any :: forall a. Show a => a -> a)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```https://gitlab.haskell.org/ghc/ghc/-/issues/18689Why check for -fdefer-type-errors in metaTyVarUpdateOK?2020-12-22T13:22:39ZRichard Eisenbergrae@richarde.devWhy check for -fdefer-type-errors in metaTyVarUpdateOK?Function `checkTypeEq` changes its behavior depending on the presence of `-fdefer-type-errors` in an obscure case around heterogeneous equalities; see the code in `go_co`. This is undocumented (in the code), and neither Simon nor I can f...Function `checkTypeEq` changes its behavior depending on the presence of `-fdefer-type-errors` in an obscure case around heterogeneous equalities; see the code in `go_co`. This is undocumented (in the code), and neither Simon nor I can figure out why it's done.
Task: figure this out, and either document or remove this behavior.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/18308Order of StandaloneKindSignatures and CUSKs extensions significant2021-03-31T15:14:45ZBjörn HegerforsOrder of StandaloneKindSignatures and CUSKs extensions significant## Summary
I have some code that compiles without the `StandaloneKindSignatures` extension, does not compile with it, but does compile again if I also add the `CUSKs` extension _after_ `StandaloneKindSignatures`. However, if I place the...## Summary
I have some code that compiles without the `StandaloneKindSignatures` extension, does not compile with it, but does compile again if I also add the `CUSKs` extension _after_ `StandaloneKindSignatures`. However, if I place the `CUSKs` extension _before_ `StandaloneKindSignatures`, then the code doesn't compile.
I'm not sure if I can avoid a CUSK in this case either, because it revolves around an associated type family, which to my understanding stand-alone kind signatures cannot (yet) be written for.
I generally try to keep my extensions arranged alphabetically, which is unfortunate in this case. But that's not at all a big worry. For now I can put `CUSKs` after `StandaloneKindSignatures` as a workaround.
## Steps to reproduce
Boiling it down to a minimal demonstrative case, this compiles:
```haskell
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE CUSKs #-}
import Data.Kind (Type)
import Data.Proxy (Proxy)
class Cls where
type Fam (k :: Type) (a :: k) :: Type
mtd :: Proxy k -> Proxy (a :: k) -> Fam k a -> Int
```
but this doesn't:
```haskell
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE CUSKs #-}
{-# LANGUAGE StandaloneKindSignatures #-}
import Data.Kind (Type)
import Data.Proxy (Proxy)
class Cls where
type Fam (k :: Type) (a :: k) :: Type
mtd :: Proxy k -> Proxy (a :: k) -> Fam k a -> Int
```
## Expected behavior
I would expect both of the above to compile.
I should also note that it's not very clear to me what it is about the type signature for `mtd` that makes it problematic. The part that is sensitive here is the `(a :: k)` kind annotation. Whether I instead put that annotation in a `forall` makes no difference. If I simply remove the kind annotation for `a`, and let it be inferred, the code compiles regardless of which of `StandaloneKindSignatures` and `CUSKs` are enabled (and in which order). I don't know if this part behaves as expected or not.
## Environment
* GHC version used: 8.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/18062A cast might get in the way of instantiation2020-04-27T10: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 kind-checks 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 kind-checks 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/17675eqType fails on comparing FunTys2022-02-21T17:09:27ZRichard Eisenbergrae@richarde.deveqType fails on comparing FunTysSuppose I have `co :: IntRep ~ r` and `a :: TYPE IntRep`. Consider `t1 = a -> ()` and `t2 = (a |> TYPE co) -> ()`. We have ``t1 `eqType` t2``, but if we call `splitTyConApp` on `t1` and `t2`, we'll get different arguments (the first arg ...Suppose I have `co :: IntRep ~ r` and `a :: TYPE IntRep`. Consider `t1 = a -> ()` and `t2 = (a |> TYPE co) -> ()`. We have ``t1 `eqType` t2``, but if we call `splitTyConApp` on `t1` and `t2`, we'll get different arguments (the first arg in `t1` will be `IntRep` while the first arg in `t2` will be `r`). This violates property EQ of Note [Non-trivial definitional equality] in TyCoRep.
The fix is easy: in `nonDetCmpTypeX`, the `FunTy` case should recur into `nonDetCmpTypeX` for both argument and result. This does a kind check. Recurring into `go` skips the kind check.
Unfortunately, there are other places that also work with equality. This list includes at least
* [ ] `TcType.tc_eq_type`
* [ ] `CoreMap`
* [ ] Pure unifier in `Unify`, which probably also needs to recur in kinds on a `FunTy`. Or maybe this works via decomposition into a `TyConApp`, so all is OK. But it needs to be checked.
I believe Simon has some preliminary work on a branch.https://gitlab.haskell.org/ghc/ghc/-/issues/17674Kill EQ12021-09-17T17:18:39ZRichard Eisenbergrae@richarde.devKill EQ1Note [Respecting definitional equality] introduces invariant EQ1:
```
(EQ1) No decomposable CastTy to the left of an AppTy, where a decomposable
cast is one that relates either a FunTy to a FunTy or a
ForAllTy to a For...Note [Respecting definitional equality] introduces invariant EQ1:
```
(EQ1) No decomposable CastTy to the left of an AppTy, where a decomposable
cast is one that relates either a FunTy to a FunTy or a
ForAllTy to a ForAllTy.
```
This invariant is a small pain to uphold. And perhaps we don't need to. If, instead, we modified `eqType` to look at the kind of arguments to `AppTy`s, then we wouldn't need EQ1, significantly simplifying `mkAppTy`. (Actually, it will just remove 2 lines. But it removes two calls to `decomposePiCos`. This will allow the one remaining call to this function to have more sway in the design of `decomposePiCos`, simplifying that bit of code, as well.)
Another nice benefit: by removing this invariant, we have an opportunity to explore different solutions to #17644, which hit a dead end in EQ1. See https://gitlab.haskell.org/ghc/ghc/issues/17644#note_245757.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/17621Type-level multiplication parsed as application at kind *, no guidance provided2020-01-05T03:00:19ZGeshType-level 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.8