GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20200120T18:20:09Zhttps://gitlab.haskell.org/ghc/ghc//issues/17644Loop in the constraint solver around variables free in kinds20200120T18:20:09ZRichard Eisenbergrae@richarde.devLoop in the constraint solver around variables free in kindsSpun off from the bowels of #17323 (https://gitlab.haskell.org/ghc/ghc/issues/17323#note_243178, https://gitlab.haskell.org/ghc/ghc/issues/17323#note_243577, https://gitlab.haskell.org/ghc/ghc/issues/17323#note_244748), but I think orthogonal to that ticket. No need to read that ticket to understand this one.
Here is a simple form of the potential problem (due to @simonpj):
```
Inert set:
[G] b ~ a
Work item:
[G] (a :: *) ~ (c :: b > *) (d :: b)
```
I think GHC will add that work item to the inert set, despite the fact that it seems loopy.
And in this example, I think we'll actually get a loop:
```
a :: e
b :: d > e
c :: d
d :: Type
e :: Type
f :: e > Type
g :: d > Type
inert set:
[D] a ~ b c
[D] e ~ g c
[G] g1 :: d ~ f a  just having `a` here would violate K3a of Note [Extending the inert equalities]
work item: [D] e ~ f a
```
Let's see what happens.
1. `can_eq_nc'` will get to its flattening clause, so both sides get flattened, yielding `[D] g c ~ f (b c)`.
2. `can_eq_nc'` then decomposes to `[D] g ~ f` and `[D] c ~ b c`. We'll continue here with the latter.
3. On the new work item `[D] c ~ b c`, `can_eq_nc'` will get to its flattening clause, so both sides get flattened, causing no change.
4. Then, we go to `canEqTyVar`. We have `c :: d` but `b c :: e`, so we flatten both kinds. We thus get `[D] (c > g1) ~ b c`, where `g1 :: d ~ f a` comes from flattening. We then emit `[D] f a ~ e`. The first is irreducible, but the second brings us right back where we started. (Note that `e` isn't rewritten by flattening because the equality for `e` is a Derived, which cannot be used to rewrite a kind.)
[This comment](https://gitlab.haskell.org/ghc/ghc/issues/17644#note_245566) below shows `f8` which shows an actual loop from this case. Plus: the other examples there show cases where simply reordering the constraints in a type changes the accept/reject behaviour; this is Bad.Spun off from the bowels of #17323 (https://gitlab.haskell.org/ghc/ghc/issues/17323#note_243178, https://gitlab.haskell.org/ghc/ghc/issues/17323#note_243577, https://gitlab.haskell.org/ghc/ghc/issues/17323#note_244748), but I think orthogonal to that ticket. No need to read that ticket to understand this one.
Here is a simple form of the potential problem (due to @simonpj):
```
Inert set:
[G] b ~ a
Work item:
[G] (a :: *) ~ (c :: b > *) (d :: b)
```
I think GHC will add that work item to the inert set, despite the fact that it seems loopy.
And in this example, I think we'll actually get a loop:
```
a :: e
b :: d > e
c :: d
d :: Type
e :: Type
f :: e > Type
g :: d > Type
inert set:
[D] a ~ b c
[D] e ~ g c
[G] g1 :: d ~ f a  just having `a` here would violate K3a of Note [Extending the inert equalities]
work item: [D] e ~ f a
```
Let's see what happens.
1. `can_eq_nc'` will get to its flattening clause, so both sides get flattened, yielding `[D] g c ~ f (b c)`.
2. `can_eq_nc'` then decomposes to `[D] g ~ f` and `[D] c ~ b c`. We'll continue here with the latter.
3. On the new work item `[D] c ~ b c`, `can_eq_nc'` will get to its flattening clause, so both sides get flattened, causing no change.
4. Then, we go to `canEqTyVar`. We have `c :: d` but `b c :: e`, so we flatten both kinds. We thus get `[D] (c > g1) ~ b c`, where `g1 :: d ~ f a` comes from flattening. We then emit `[D] f a ~ e`. The first is irreducible, but the second brings us right back where we started. (Note that `e` isn't rewritten by flattening because the equality for `e` is a Derived, which cannot be used to rewrite a kind.)
[This comment](https://gitlab.haskell.org/ghc/ghc/issues/17644#note_245566) below shows `f8` which shows an actual loop from this case. Plus: the other examples there show cases where simply reordering the constraints in a type changes the accept/reject behaviour; this is Bad.https://gitlab.haskell.org/ghc/ghc//issues/17633Closed type family declaration accepts any name in LHS20200103T21:33:08ZMaxim KoltsovClosed type family declaration accepts any name in LHS## Summary
Closed type family declaration will accept (almost) any name instead of family's name left of `=`.
## Steps to reproduce
```haskell
{# LANGUAGE TypeFamilies #}
module WTF where
type family Bar (a :: *) :: * where
Bar Int = ()
type family Foo (a :: *) :: * where
Bar Int = Bool
Bar Bool = Int
Bar a = a
```
When loaded to ghci, this file not only compiles, but works as if `Foo` were defined the normal way:
```
λ> :kind! Bar Int
Bar Int :: *
= ()
λ> :kind! Bar Bool
Bar Bool :: *
= Bar Bool
λ> :kind! Foo Int
Foo Int :: *
= Bool
λ> :kind! Foo Bool
Foo Bool :: *
= Int
λ> :kind! Foo Char
Foo Char :: *
= Char
```
It's clear that `Foo` is defined as it should be and that `Bar` is not broken by this definition.
## Expected behavior
GHC should emit an error in this case, as this code seems very strange.
Curiously, if `Bar` is not in scope GHC detects an error at `Foo`'s definition:
```
<interactive>:5:3: error:
Not in scope: type constructor or class ‘Bar’
```
Moreover, if I try to use some family from another module, it fails as well:
```
> import GHC.Generics
> :{
 type family Foo (a :: *) where
 Rep Bool = Maybe
 :}
<interactive>:6:3: error:
• Mismatched type name in type family instance.
Expected: Foo
Actual: Rep
```
## Environment
* GHC version used:
```console
$ stack exec  ghc V
The Glorious Glasgow Haskell Compilation System, version 8.6.3
```
* Operating System: macOS## Summary
Closed type family declaration will accept (almost) any name instead of family's name left of `=`.
## Steps to reproduce
```haskell
{# LANGUAGE TypeFamilies #}
module WTF where
type family Bar (a :: *) :: * where
Bar Int = ()
type family Foo (a :: *) :: * where
Bar Int = Bool
Bar Bool = Int
Bar a = a
```
When loaded to ghci, this file not only compiles, but works as if `Foo` were defined the normal way:
```
λ> :kind! Bar Int
Bar Int :: *
= ()
λ> :kind! Bar Bool
Bar Bool :: *
= Bar Bool
λ> :kind! Foo Int
Foo Int :: *
= Bool
λ> :kind! Foo Bool
Foo Bool :: *
= Int
λ> :kind! Foo Char
Foo Char :: *
= Char
```
It's clear that `Foo` is defined as it should be and that `Bar` is not broken by this definition.
## Expected behavior
GHC should emit an error in this case, as this code seems very strange.
Curiously, if `Bar` is not in scope GHC detects an error at `Foo`'s definition:
```
<interactive>:5:3: error:
Not in scope: type constructor or class ‘Bar’
```
Moreover, if I try to use some family from another module, it fails as well:
```
> import GHC.Generics
> :{
 type family Foo (a :: *) where
 Rep Bool = Maybe
 :}
<interactive>:6:3: error:
• Mismatched type name in type family instance.
Expected: Foo
Actual: Rep
```
## Environment
* GHC version used:
```console
$ stack exec  ghc V
The Glorious Glasgow Haskell Compilation System, version 8.6.3
```
* Operating System: macOS8.8.1https://gitlab.haskell.org/ghc/ghc//issues/17625Evidence for equality constraints on typeclass methods isn’t erased20200108T16:45:20ZAlexis KingEvidence for equality constraints on typeclass methods isn’t erasedGenerally, I expect `a ~ b` constraints to have no runtime cost, so I was surprised to discover that they sometimes do. If I understand correctly, constraints of type `a ~ b` are boxed versions of `a ~# b`, the latter of which have no runtime representation. Ordinarily, this boxing and unboxing is eliminated via worker/wrapper just like any other boxing, but worker/wrapper can only be performed at call sites to known functions, so equality constraints on typeclass methods are not erased unless the method is specialized. This program illustrates that:
```haskell
{# LANGUAGE ConstrainedClassMethods, TypeFamilies #}
module M where
type family F a
class C a where
m :: F a ~ Int => a > Bool
f :: (C a, F a ~ Int) => a > Bool
f x = not (m x)
```
Compiling with `O ddumpsimpl` reveals that the call to `m` inside `F a ~ Int` really does pass a boxed equality.
This seems silly to me. As far as I can tell, equalities are aggressively forced, so it would be entirely safe to perform a worker/wrapperesque transformation to the `C` constructor itself. Specifically, GHC could desugar `C` into the following:
```haskell
newtype C a = $WC { $wm :: F a ~# Int > a > Bool }
C :: (F a ~ Int => a > Bool) > C a
C m = $WC { $wm = m `seq` \co > m (Eq# co) }
m :: (C a, F a ~ Int) => a > Bool
m ($WC { $wm }) (Eq# co) = $wm co
```
The equality argument would be erased on both ends via the same mechanism that exists today for worker/wrapper DataCons, and the resulting program would be slightly more efficient.
Maybe there is some problem with this scheme I’m not seeing; it’s entirely possible. I don’t know all the subtleties. But seeing as it seems totally sound to me based on the investigation I’ve done so far, and since equalities *not* being erased was so surprising to me, I feel like it isn’t entirely unreasonable to consider this a bug rather than a missing feature (though that is admittedly arguable).Generally, I expect `a ~ b` constraints to have no runtime cost, so I was surprised to discover that they sometimes do. If I understand correctly, constraints of type `a ~ b` are boxed versions of `a ~# b`, the latter of which have no runtime representation. Ordinarily, this boxing and unboxing is eliminated via worker/wrapper just like any other boxing, but worker/wrapper can only be performed at call sites to known functions, so equality constraints on typeclass methods are not erased unless the method is specialized. This program illustrates that:
```haskell
{# LANGUAGE ConstrainedClassMethods, TypeFamilies #}
module M where
type family F a
class C a where
m :: F a ~ Int => a > Bool
f :: (C a, F a ~ Int) => a > Bool
f x = not (m x)
```
Compiling with `O ddumpsimpl` reveals that the call to `m` inside `F a ~ Int` really does pass a boxed equality.
This seems silly to me. As far as I can tell, equalities are aggressively forced, so it would be entirely safe to perform a worker/wrapperesque transformation to the `C` constructor itself. Specifically, GHC could desugar `C` into the following:
```haskell
newtype C a = $WC { $wm :: F a ~# Int > a > Bool }
C :: (F a ~ Int => a > Bool) > C a
C m = $WC { $wm = m `seq` \co > m (Eq# co) }
m :: (C a, F a ~ Int) => a > Bool
m ($WC { $wm }) (Eq# co) = $wm co
```
The equality argument would be erased on both ends via the same mechanism that exists today for worker/wrapper DataCons, and the resulting program would be slightly more efficient.
Maybe there is some problem with this scheme I’m not seeing; it’s entirely possible. I don’t know all the subtleties. But seeing as it seems totally sound to me based on the investigation I’ve done so far, and since equalities *not* being erased was so surprising to me, I feel like it isn’t entirely unreasonable to consider this a bug rather than a missing feature (though that is admittedly arguable).https://gitlab.haskell.org/ghc/ghc//issues/17567Never `Any`ify during kind inference20210111T13: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
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, toplevel 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 addon to any of the above plans. Because `Type` is not always wellkinded, 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 toplevel 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 contextbuilding in Option E for good effect. This is the first solution I'm actually happy with.
Thoughts?#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, toplevel 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 addon to any of the above plans. Because `Type` is not always wellkinded, 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 toplevel 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 contextbuilding in Option E for good effect. This is the first solution I'm actually happy with.
Thoughts?https://gitlab.haskell.org/ghc/ghc//issues/17564Don't drop derived quantified constraints20191211T09:48:10ZRichard Eisenbergrae@richarde.devDon't drop derived quantified constraintsIn looking at the way quantified constraints are handled, I noticed that we drop derived quantified constraints (in `TcCanonical.solveForAll`). I don't see a reason why this is a good idea. And indeed, it causes trouble:
```hs
{# LANGUAGE QuantifiedConstraints, MultiParamTypeClasses,
KindSignatures, FlexibleInstances, TypeFamilies #}
module Bug where
import Data.Kind
class (forall (a :: Type > Type). a b ~ a c) => C b c
instance C a a
class (b ~ c) => D b c
instance D a a
foo :: C a b => a > b
foo = undefined
bar = foo
food :: D a b => a > b
food = undefined
bard = food
```
`C` and `D` should really behave identically. Yet `bar` is rejected while `bard` is accepted.
Note that the monomorphism restriction forces us to solve, not quantify over, the `C` and `D` constraints. This is intentional in this test case.
Normally, the superclasses of a wanted are emitted as derived constraints. In the case of `bard`, we start with `[W] D alpha beta`, which doesn't make progress. So we get `[D] alpha ~ beta`, which unifies the two, and then `[W] D alpha alpha` is easily dispatched. But in `bar` the `[D] forall a. a alpha ~ a beta` is dropped, leading to rejection.
The kind signature in the test case is needed because of #17562.In looking at the way quantified constraints are handled, I noticed that we drop derived quantified constraints (in `TcCanonical.solveForAll`). I don't see a reason why this is a good idea. And indeed, it causes trouble:
```hs
{# LANGUAGE QuantifiedConstraints, MultiParamTypeClasses,
KindSignatures, FlexibleInstances, TypeFamilies #}
module Bug where
import Data.Kind
class (forall (a :: Type > Type). a b ~ a c) => C b c
instance C a a
class (b ~ c) => D b c
instance D a a
foo :: C a b => a > b
foo = undefined
bar = foo
food :: D a b => a > b
food = undefined
bard = food
```
`C` and `D` should really behave identically. Yet `bar` is rejected while `bard` is accepted.
Note that the monomorphism restriction forces us to solve, not quantify over, the `C` and `D` constraints. This is intentional in this test case.
Normally, the superclasses of a wanted are emitted as derived constraints. In the case of `bard`, we start with `[W] D alpha beta`, which doesn't make progress. So we get `[D] alpha ~ beta`, which unifies the two, and then `[W] D alpha alpha` is easily dispatched. But in `bar` the `[D] forall a. a alpha ~ a beta` is dropped, leading to rejection.
The kind signature in the test case is needed because of #17562.https://gitlab.haskell.org/ghc/ghc//issues/17563Validity check quantified constraints20201213T22:02:03ZRichard Eisenbergrae@richarde.devValidity check quantified constraintsThis module is accepted:
```hs
{# LANGUAGE QuantifiedConstraints #}
module Bug2 where
blah :: (forall a. a b ~ a c) => b > c
blah = undefined
```
But it shouldn't be: it uses `~` with neither `GADTs` nor `TypeFamilies` enabled.This module is accepted:
```hs
{# LANGUAGE QuantifiedConstraints #}
module Bug2 where
blah :: (forall a. a b ~ a c) => b > c
blah = undefined
```
But it shouldn't be: it uses `~` with neither `GADTs` nor `TypeFamilies` enabled.8.10.2https://gitlab.haskell.org/ghc/ghc//issues/17562`Any` appearing in a quantified constraint20210111T13:07:45ZRichard Eisenbergrae@richarde.dev`Any` appearing in a quantified constraintIf I say
```hs
{# LANGUAGE QuantifiedConstraints, MultiParamTypeClasses #}
module Bug where
class (forall a. a b ~ a c) => C b c
```
I get
```
Bug.hs:5:1: error:
• Illegal type synonym family application ‘GHC.Types.Any
@*’ in instance:
(a b :: GHC.Types.Any @*) ~ (a c :: GHC.Types.Any @*)
• In the quantified constraint ‘forall (a :: k > GHC.Types.Any).
a b ~ a c’
In the context: forall (a :: k > GHC.Types.Any). a b ~ a c
While checking the superclasses of class ‘C’
In the class declaration for ‘C’

5  class (forall a. a b ~ a c) => C b c
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This is a specific case of #17567. Despite superficial similarity, this is unrelated to #16775.If I say
```hs
{# LANGUAGE QuantifiedConstraints, MultiParamTypeClasses #}
module Bug where
class (forall a. a b ~ a c) => C b c
```
I get
```
Bug.hs:5:1: error:
• Illegal type synonym family application ‘GHC.Types.Any
@*’ in instance:
(a b :: GHC.Types.Any @*) ~ (a c :: GHC.Types.Any @*)
• In the quantified constraint ‘forall (a :: k > GHC.Types.Any).
a b ~ a c’
In the context: forall (a :: k > GHC.Types.Any). a b ~ a c
While checking the superclasses of class ‘C’
In the class declaration for ‘C’

5  class (forall a. a b ~ a c) => C b c
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This is a specific case of #17567. Despite superficial similarity, this is unrelated to #16775.9.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/17545Coercion variables appearing where they shouldn't20200120T00:24:32ZKrzysztof GogolewskiCoercion variables appearing where they shouldn'tDuring review of !2268, we've discovered a few places where a coercion variable can appear where it shouldn't. Those are calls to "OrCoVar" functions in:
* [ ] `newLocal` in `MkId`
* [ ] `bindIfaceId` in `TcIface`
* [ ] `tcPatBndr` in `TcPat`
that happen when running tests T13990 T14285 T15648.
The goal is to fix this, or come up with a convincing reason that a coercion makes sense there.During review of !2268, we've discovered a few places where a coercion variable can appear where it shouldn't. Those are calls to "OrCoVar" functions in:
* [ ] `newLocal` in `MkId`
* [ ] `bindIfaceId` in `TcIface`
* [ ] `tcPatBndr` in `TcPat`
that happen when running tests T13990 T14285 T15648.
The goal is to fix this, or come up with a convincing reason that a coercion makes sense there.https://gitlab.haskell.org/ghc/ghc//issues/17541Regression involving unboxed types and type families20191212T16:20:40ZMatthew PickeringRegression involving unboxed types and type familiesThis program compiles with 8.6.5 and 8.8.1 but not with HEAD.
```
{# LANGUAGE
MagicHash,
FlexibleInstances,
MultiParamTypeClasses,
TypeFamilies,
PolyKinds,
DataKinds,
FunctionalDependencies,
TypeFamilyDependencies #}
module A where
import GHC.Prim
import GHC.Exts
type family Rep rep where
Rep Int = IntRep
type family Unboxed rep = (urep :: TYPE (Rep rep))  urep > rep where
Unboxed Int = Int#
```
```
[1 of 1] Compiling A ( A.hs, A.o )
A.hs:20:17: error:
• Expected kind ‘TYPE (Rep rep)’,
but ‘Int#’ has kind ‘TYPE 'IntRep’
• In the type ‘Int#’
In the type family declaration for ‘Unboxed’

20  Unboxed Int = Int#
 ^^^^
```This program compiles with 8.6.5 and 8.8.1 but not with HEAD.
```
{# LANGUAGE
MagicHash,
FlexibleInstances,
MultiParamTypeClasses,
TypeFamilies,
PolyKinds,
DataKinds,
FunctionalDependencies,
TypeFamilyDependencies #}
module A where
import GHC.Prim
import GHC.Exts
type family Rep rep where
Rep Int = IntRep
type family Unboxed rep = (urep :: TYPE (Rep rep))  urep > rep where
Unboxed Int = Int#
```
```
[1 of 1] Compiling A ( A.hs, A.o )
A.hs:20:17: error:
• Expected kind ‘TYPE (Rep rep)’,
but ‘Int#’ has kind ‘TYPE 'IntRep’
• In the type ‘Int#’
In the type family declaration for ‘Unboxed’

20  Unboxed Int = Int#
 ^^^^
```https://gitlab.haskell.org/ghc/ghc//issues/17432Wildcards in standalone kind signatures20200112T20:22:51ZRichard Eisenbergrae@richarde.devWildcards in standalone kind signaturesWe should allow partial kind signatures as well as partial type signatures:
```hs
type Maybe :: _ > Type
data Maybe a = Nothing  Just a
type Proxy :: forall (k :: _). k > _
data Proxy = MkP
```
Of course, this would mean that polymorphic recursion would not be allowed. It's all just like at the term level.We should allow partial kind signatures as well as partial type signatures:
```hs
type Maybe :: _ > Type
data Maybe a = Nothing  Just a
type Proxy :: forall (k :: _). k > _
data Proxy = MkP
```
Of course, this would mean that polymorphic recursion would not be allowed. It's all just like at the term level.https://gitlab.haskell.org/ghc/ghc//issues/17395`tcMatchTy` is terribly broken20191101T09:28:24ZSimon Peyton Jones`tcMatchTy` is terribly brokenSuppose `(T :: forall k. k > Type)` and we are matching
```
tcMatchTy (T k (a::k)) (T j (b::j))
```
Then we'll match `k :> j`, as expected. But then in `TcUnify.unify_tys`
we invoke
```
unify_tys env (a::k) (b::j) (Refl k)
```
Despite `Note [Kind coercions in Unify]` it's not clear to
me why we need that Refl coercion.
But, assuming we need it, very very bad things now happen.
In `uUnrefined` we end up adding the binding `a :> (b > Refl k)`.
Alas! Alack! `k` is one of the template variables, which we are
substituting away, so it's **terrible** if `k` appears in the
range of the substitution  it belongs only in the range.
A oneline (actually onecharacter) fix is this:
```
 = do { unify_ty env x y (mkNomReflCo $ typeKind x)
+ = do { unify_ty env x y (mkNomReflCo $ typeKind y)
```
But I am hardpressed to explain exactly why this is the correct fix.
@rae, help?
This actually bit me when working on `mkCastTy` in #17323.Suppose `(T :: forall k. k > Type)` and we are matching
```
tcMatchTy (T k (a::k)) (T j (b::j))
```
Then we'll match `k :> j`, as expected. But then in `TcUnify.unify_tys`
we invoke
```
unify_tys env (a::k) (b::j) (Refl k)
```
Despite `Note [Kind coercions in Unify]` it's not clear to
me why we need that Refl coercion.
But, assuming we need it, very very bad things now happen.
In `uUnrefined` we end up adding the binding `a :> (b > Refl k)`.
Alas! Alack! `k` is one of the template variables, which we are
substituting away, so it's **terrible** if `k` appears in the
range of the substitution  it belongs only in the range.
A oneline (actually onecharacter) fix is this:
```
 = do { unify_ty env x y (mkNomReflCo $ typeKind x)
+ = do { unify_ty env x y (mkNomReflCo $ typeKind y)
```
But I am hardpressed to explain exactly why this is the correct fix.
@rae, help?
This actually bit me when working on `mkCastTy` in #17323.8.10.1https://gitlab.haskell.org/ghc/ghc//issues/17368Implement homogeneous equality20200310T14:21:59ZRichard Eisenbergrae@richarde.devImplement homogeneous equalityAs observed in [two](https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1076&context=compsci_pubs) [papers](https://richarde.dev/papers/2019/deproles/deproles.pdf), the primitive equality type in GHC can be made homogeneous. This is both a simplification over the status quo (heterogeneous equality) and an important step toward implementing dependent types.
This ticket is to track this change.
Step 1: Modify the typechecker to use predicates instead of types internally. This will essentially be a glorification of `PredTree` (renamed `Pred`), and a `CtEvidence` will now store a `Pred`, not a `PredType`.
See also https://gitlab.haskell.org/ghc/ghc/wikis/dependenthaskell/phase2, which has much discussion.As observed in [two](https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1076&context=compsci_pubs) [papers](https://richarde.dev/papers/2019/deproles/deproles.pdf), the primitive equality type in GHC can be made homogeneous. This is both a simplification over the status quo (heterogeneous equality) and an important step toward implementing dependent types.
This ticket is to track this change.
Step 1: Modify the typechecker to use predicates instead of types internally. This will essentially be a glorification of `PredTree` (renamed `Pred`), and a `CtEvidence` will now store a `Pred`, not a `PredType`.
See also https://gitlab.haskell.org/ghc/ghc/wikis/dependenthaskell/phase2, which has much discussion.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/17367Letbound wildcards are not letgeneralised20200205T23:07:07ZSebastian GrafLetbound wildcards are not letgeneralisedWith `XBangPatterns`, the act of declaring a letbinding without using it might have a sideeffect. Consider this example:
```haskell
{# LANGUAGE BangPatterns #}
f :: ()
f = let !x = undefined in ()
g :: ()
g = let !_ = undefined in ()
main = do
print f
print g
```
Both `f` and `g` declare a variable in a strict binding that is actually dead. Surprisingly, they lead to different code. Here's the Core (GHC 8.6.5) after optimisation:
```
main
= >>
(print
@ ()
GHC.Show.$fShow()
(case \ (@ a_a2hW) >
undefined
@ 'GHC.Types.LiftedRep
@ a_a2hW
(<snip>)
of
{ __DEFAULT >
GHC.Tuple.()
}))
(print
@ ()
GHC.Show.$fShow()
(case undefined
@ 'GHC.Types.LiftedRep
@ GHC.Types.Any
(<snip>)
of
{ __DEFAULT >
GHC.Tuple.()
}))
```
Note the `/\a. undefined @LiftedRep @a` in the first scrutinee. This is ultimately due to the fact that `x` is letgeneralised, whereas `_` is not. The first case is on a lambda, so I expect it to perform no forcing at all. The first case evaluates a complete application of `undefined`, so should crash. As a result, I'd expect this program to generate the following output:
```
()
test: Prelude.undefined
CallStack (from HasCallStack):
error, called at libraries/base/GHC/Err.hs:78:14 in base:GHC.Err
undefined, called at test.hs:4:15 in main:Main
```
Currently (tested on GHC 8.6.5), even the first `print f` will crash, so the behavior is actually consistent. I think this is actually a reasonable semantics, but I didn't expect it based on the difference in Core. My understanding of Core semantics might be off here.
So: Is letgeneralisation of `x` but not of `_` expected? If so, why does `let !x = undefined in ()` crash?
CC @simonpj @rae since this is a continuation of the discussion in https://gitlab.haskell.org/ghc/ghc/merge_requests/1954#note_229057.With `XBangPatterns`, the act of declaring a letbinding without using it might have a sideeffect. Consider this example:
```haskell
{# LANGUAGE BangPatterns #}
f :: ()
f = let !x = undefined in ()
g :: ()
g = let !_ = undefined in ()
main = do
print f
print g
```
Both `f` and `g` declare a variable in a strict binding that is actually dead. Surprisingly, they lead to different code. Here's the Core (GHC 8.6.5) after optimisation:
```
main
= >>
(print
@ ()
GHC.Show.$fShow()
(case \ (@ a_a2hW) >
undefined
@ 'GHC.Types.LiftedRep
@ a_a2hW
(<snip>)
of
{ __DEFAULT >
GHC.Tuple.()
}))
(print
@ ()
GHC.Show.$fShow()
(case undefined
@ 'GHC.Types.LiftedRep
@ GHC.Types.Any
(<snip>)
of
{ __DEFAULT >
GHC.Tuple.()
}))
```
Note the `/\a. undefined @LiftedRep @a` in the first scrutinee. This is ultimately due to the fact that `x` is letgeneralised, whereas `_` is not. The first case is on a lambda, so I expect it to perform no forcing at all. The first case evaluates a complete application of `undefined`, so should crash. As a result, I'd expect this program to generate the following output:
```
()
test: Prelude.undefined
CallStack (from HasCallStack):
error, called at libraries/base/GHC/Err.hs:78:14 in base:GHC.Err
undefined, called at test.hs:4:15 in main:Main
```
Currently (tested on GHC 8.6.5), even the first `print f` will crash, so the behavior is actually consistent. I think this is actually a reasonable semantics, but I didn't expect it based on the difference in Core. My understanding of Core semantics might be off here.
So: Is letgeneralisation of `x` but not of `_` expected? If so, why does `let !x = undefined in ()` crash?
CC @simonpj @rae since this is a continuation of the discussion in https://gitlab.haskell.org/ghc/ghc/merge_requests/1954#note_229057.https://gitlab.haskell.org/ghc/ghc//issues/17343BangPatterns in PatternGuards don't work like docs would suggest20191016T11:38:42ZJakob BrünkerBangPatterns in PatternGuards don't work like docs would suggest## Summary and Steps to reproduce
The docs don't seem to say anything special about the interaction between bang patterns and pattern guards, so I wouldn't expect them to work any differently there. And yet:
```haskell
let f = case undefined of !_ > () in f  (a) fails (as expected)
let f  let !_ = undefined = () in f  (b) fails (as expected)
let f  !_ < undefined = () in f  (c) succeeds...
```
## Expected behavior
I would expect `(c)` to fail, in the same way as `(a)` and `(b)` do.
Alternatively, an explanation for how BangPatterns interact with PatternGuards could be added to the "Bang patterns" section in `glasgow_exts.rst`.
## Environment
* GHC version used: 8.6.5, 8.8.1## Summary and Steps to reproduce
The docs don't seem to say anything special about the interaction between bang patterns and pattern guards, so I wouldn't expect them to work any differently there. And yet:
```haskell
let f = case undefined of !_ > () in f  (a) fails (as expected)
let f  let !_ = undefined = () in f  (b) fails (as expected)
let f  !_ < undefined = () in f  (c) succeeds...
```
## Expected behavior
I would expect `(c)` to fail, in the same way as `(a)` and `(b)` do.
Alternatively, an explanation for how BangPatterns interact with PatternGuards could be added to the "Bang patterns" section in `glasgow_exts.rst`.
## Environment
* GHC version used: 8.6.5, 8.8.18.10.1Sebastian GrafSebastian Grafhttps://gitlab.haskell.org/ghc/ghc//issues/17333Coercible solver does not look through "class newtypes"20210216T21:35:31ZRyan ScottCoercible solver does not look through "class newtypes"The code below makes use of the "class newtype" design pattern:
```hs
class Show a => MyShow a
instance Show a => MyShow a
```
`MyShow` is a newtype around `Show` in the sense that when compiled to Core, a `MyShow` dictionary is literally a newtype around `Show`. Unfortunately, this newtype treatment does not extend to the `Coercible` solver, as the following example demonstrates:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE MonoLocalBinds #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE UndecidableInstances #}
{# LANGUAGE UndecidableSuperClasses #}
module Bug where
import Data.Coerce
class Show a => MyShow a
instance Show a => MyShow a
newtype T1 a = MkT1 ( Show a => a > a > String)
newtype T2 a = MkT2 (MyShow a => a > a > String)
f :: T1 a > T2 a
f = coerce
```
```
$ /opt/ghc/8.8.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:20:5: error:
• Couldn't match representation of type ‘MyShow a’
with that of ‘Show a’
arising from a use of ‘coerce’
The data constructor ‘Bug.C:MyShow’
of newtype ‘MyShow’ is not in scope
• In the expression: coerce
In an equation for ‘f’: f = coerce
• Relevant bindings include
f :: T1 a > T2 a (bound at Bug.hs:20:1)

20  f = coerce
 ^^^^^^
```
Somewhat surprisingly, this does not work. Even the error message indicates that `MyShow` is a newtype (which is a bit odd, but whatever), but since the internal `C:MyShow` constructor is not exposed, the `Coercible` solver doesn't have enough information to proceed.
If the following change is applied to GHC, then it typechecks:
```diff
diff git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs
index a339dd7b57..8640b3e3e0 100644
 a/compiler/typecheck/FamInst.hs
+++ b/compiler/typecheck/FamInst.hs
@@ 41,7 +41,7 @@ import Name
import Pair
import Panic
import VarSet
import Bag( Bag, unionBags, unitBag )
+import Bag( Bag, emptyBag, unionBags, unitBag )
import Control.Monad
#include "HsVersions.h"
@@ 577,6 +577,10 @@ tcTopNormaliseNewTypeTF_maybe faminsts rdr_env ty
= mapStepResult (\co > (unitBag gre, co)) $
unwrapNewTypeStepper rec_nts tc tys
+  isClassTyCon tc && isNewTyCon tc
+ = mapStepResult (\co > (emptyBag, co)) $
+ unwrapNewTypeStepper rec_nts tc tys
+
 otherwise
= NS_Done
```
The simplified example above is somewhat contrived, although I have legitimate need of this feature in more complicated scenarios like this one (inspired by [Generic Programming of All Kinds](https://victorcmiraldo.github.io/data/hask2018_draft.pdf)):
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE DataKinds #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE GADTs #}
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE UndecidableInstances #}
{# LANGUAGE UndecidableSuperClasses #}
module GOAK where
import Data.Coerce
import Data.Kind
newtype T = MkT ((forall a. Show a) => Int)
type TRep = Field (ForAllQ (Kon Show :@: Var VZ) :=>>: Kon Int) LoT0
f :: T > TRep
f (MkT x) = Field (coerce @((forall a. Show a) => Int)
@(Interpret (ForAllQ (Kon Show :@: Var VZ) :=>>: Kon Int) LoT0)
x)

infixr 5 :&&:
data LoT :: Type > Type where
LoT0 :: LoT Type
(:&&:) :: k > LoT ks > LoT (k > ks)
type family HeadLoT (tys :: LoT (k > k')) :: k where
HeadLoT (a :&&: _) = a
type family TailLoT (tys :: LoT (k > k')) :: LoT k' where
TailLoT (_ :&&: as) = as
data TyVar :: Type > Type > Type where
VZ :: TyVar (x > xs) x
VS :: TyVar xs k > TyVar (x > xs) k
data Atom :: Type > Type > Type where
Var :: TyVar d k > Atom d k
Kon :: k > Atom d k
(:@:) :: Atom d (k1 > k2) > Atom d k1 > Atom d k2
(:=>>:) :: Atom d Constraint > Atom d Type > Atom d Type
ForAllQ :: Atom (d1 > d) Constraint > Atom d Constraint
type family InterpretVar (t :: TyVar d k) (tys :: LoT d) :: k where
InterpretVar 'VZ tys = HeadLoT tys
InterpretVar ('VS v) tys = InterpretVar v (TailLoT tys)
type family Interpret (t :: Atom d k) (tys :: LoT d) :: k where
Interpret ('Var v) tys = InterpretVar v tys
Interpret ('Kon t) tys = t
Interpret (f ':@: x) tys = (Interpret f tys) (Interpret x tys)
Interpret (c ':=>>: f) tys = SuchThatI c f tys
Interpret (ForAllQ f) tys = ForAllQI f tys
newtype SuchThatI :: Atom d Constraint > Atom d Type > LoT d > Type where
SuchThatI :: (Interpret c tys => Interpret f tys) > SuchThatI c f tys
class (forall t. WrappedQI f (t ':&&: tys)) => ForAllQI (f :: Atom (d1 > d) Constraint) (tys :: LoT d)
instance (forall t. WrappedQI f (t ':&&: tys)) => ForAllQI (f :: Atom (d1 > d) Constraint) (tys :: LoT d)
class Interpret f tys => WrappedQI (f :: Atom d Constraint) (tys :: LoT d)
instance Interpret f tys => WrappedQI (f :: Atom d Constraint) (tys :: LoT d)
newtype Field :: Atom d Type > LoT d > Type where
Field :: { unField :: Interpret t x } > Field t x
```
`f` will not typecheck without the ability to coerce from `ForAllQI f tys` to `forall t. WrappedQI f (t ':&&: tys)`. Moreover, it would be extremely difficult to write `f` _without_ `coerce`.The code below makes use of the "class newtype" design pattern:
```hs
class Show a => MyShow a
instance Show a => MyShow a
```
`MyShow` is a newtype around `Show` in the sense that when compiled to Core, a `MyShow` dictionary is literally a newtype around `Show`. Unfortunately, this newtype treatment does not extend to the `Coercible` solver, as the following example demonstrates:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE MonoLocalBinds #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE UndecidableInstances #}
{# LANGUAGE UndecidableSuperClasses #}
module Bug where
import Data.Coerce
class Show a => MyShow a
instance Show a => MyShow a
newtype T1 a = MkT1 ( Show a => a > a > String)
newtype T2 a = MkT2 (MyShow a => a > a > String)
f :: T1 a > T2 a
f = coerce
```
```
$ /opt/ghc/8.8.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:20:5: error:
• Couldn't match representation of type ‘MyShow a’
with that of ‘Show a’
arising from a use of ‘coerce’
The data constructor ‘Bug.C:MyShow’
of newtype ‘MyShow’ is not in scope
• In the expression: coerce
In an equation for ‘f’: f = coerce
• Relevant bindings include
f :: T1 a > T2 a (bound at Bug.hs:20:1)

20  f = coerce
 ^^^^^^
```
Somewhat surprisingly, this does not work. Even the error message indicates that `MyShow` is a newtype (which is a bit odd, but whatever), but since the internal `C:MyShow` constructor is not exposed, the `Coercible` solver doesn't have enough information to proceed.
If the following change is applied to GHC, then it typechecks:
```diff
diff git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs
index a339dd7b57..8640b3e3e0 100644
 a/compiler/typecheck/FamInst.hs
+++ b/compiler/typecheck/FamInst.hs
@@ 41,7 +41,7 @@ import Name
import Pair
import Panic
import VarSet
import Bag( Bag, unionBags, unitBag )
+import Bag( Bag, emptyBag, unionBags, unitBag )
import Control.Monad
#include "HsVersions.h"
@@ 577,6 +577,10 @@ tcTopNormaliseNewTypeTF_maybe faminsts rdr_env ty
= mapStepResult (\co > (unitBag gre, co)) $
unwrapNewTypeStepper rec_nts tc tys
+  isClassTyCon tc && isNewTyCon tc
+ = mapStepResult (\co > (emptyBag, co)) $
+ unwrapNewTypeStepper rec_nts tc tys
+
 otherwise
= NS_Done
```
The simplified example above is somewhat contrived, although I have legitimate need of this feature in more complicated scenarios like this one (inspired by [Generic Programming of All Kinds](https://victorcmiraldo.github.io/data/hask2018_draft.pdf)):
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE DataKinds #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE GADTs #}
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE UndecidableInstances #}
{# LANGUAGE UndecidableSuperClasses #}
module GOAK where
import Data.Coerce
import Data.Kind
newtype T = MkT ((forall a. Show a) => Int)
type TRep = Field (ForAllQ (Kon Show :@: Var VZ) :=>>: Kon Int) LoT0
f :: T > TRep
f (MkT x) = Field (coerce @((forall a. Show a) => Int)
@(Interpret (ForAllQ (Kon Show :@: Var VZ) :=>>: Kon Int) LoT0)
x)

infixr 5 :&&:
data LoT :: Type > Type where
LoT0 :: LoT Type
(:&&:) :: k > LoT ks > LoT (k > ks)
type family HeadLoT (tys :: LoT (k > k')) :: k where
HeadLoT (a :&&: _) = a
type family TailLoT (tys :: LoT (k > k')) :: LoT k' where
TailLoT (_ :&&: as) = as
data TyVar :: Type > Type > Type where
VZ :: TyVar (x > xs) x
VS :: TyVar xs k > TyVar (x > xs) k
data Atom :: Type > Type > Type where
Var :: TyVar d k > Atom d k
Kon :: k > Atom d k
(:@:) :: Atom d (k1 > k2) > Atom d k1 > Atom d k2
(:=>>:) :: Atom d Constraint > Atom d Type > Atom d Type
ForAllQ :: Atom (d1 > d) Constraint > Atom d Constraint
type family InterpretVar (t :: TyVar d k) (tys :: LoT d) :: k where
InterpretVar 'VZ tys = HeadLoT tys
InterpretVar ('VS v) tys = InterpretVar v (TailLoT tys)
type family Interpret (t :: Atom d k) (tys :: LoT d) :: k where
Interpret ('Var v) tys = InterpretVar v tys
Interpret ('Kon t) tys = t
Interpret (f ':@: x) tys = (Interpret f tys) (Interpret x tys)
Interpret (c ':=>>: f) tys = SuchThatI c f tys
Interpret (ForAllQ f) tys = ForAllQI f tys
newtype SuchThatI :: Atom d Constraint > Atom d Type > LoT d > Type where
SuchThatI :: (Interpret c tys => Interpret f tys) > SuchThatI c f tys
class (forall t. WrappedQI f (t ':&&: tys)) => ForAllQI (f :: Atom (d1 > d) Constraint) (tys :: LoT d)
instance (forall t. WrappedQI f (t ':&&: tys)) => ForAllQI (f :: Atom (d1 > d) Constraint) (tys :: LoT d)
class Interpret f tys => WrappedQI (f :: Atom d Constraint) (tys :: LoT d)
instance Interpret f tys => WrappedQI (f :: Atom d Constraint) (tys :: LoT d)
newtype Field :: Atom d Type > LoT d > Type where
Field :: { unField :: Interpret t x } > Field t x
```
`f` will not typecheck without the ability to coerce from `ForAllQI f tys` to `forall t. WrappedQI f (t ':&&: tys)`. Moreover, it would be extremely difficult to write `f` _without_ `coerce`.https://gitlab.haskell.org/ghc/ghc//issues/17328GeneralizedNewtypeDeriving should not require that constructor be in scope20200703T17:15:30ZRichard Eisenbergrae@richarde.devGeneralizedNewtypeDeriving should not require that constructor be in scopeAs I learned perusing !1916 (but you don't need to read that MR), `GeneralizedNewtypeDeriving` requires that the constructor of the newtype in question be in scope. Yet this isn't really necessary:
A.hs:
```hs
module A where
newtype N1 = MkN1 N2
newtype N2 = MkN2 N1
instance Eq N2 where
(==) = const (const False)
```
B.hs:
```hs
{# LANGUAGE DerivingStrategies, StandaloneDeriving, GeneralizedNewtypeDeriving,
DerivingVia #}
module B where
import A ( N1, N2(..) )
import Data.Coerce
 This fails:
 deriving newtype instance Eq N1
 This succeeds:
 deriving via N2 instance Eq N1
 This succeeds:
instance Eq N1 where
(==) = coerce ((==) :: N2 > N2 > Bool)
```
I would think that the three possible instance declarations in B.hs would all be completely equivalent. Yet the first is rejected while the last two are accepted.
This example is indeed silly, but it's possible to make mutuallyrecursive newtypes that are not silly (by using e.g. `Maybe` or `Either` to break the loop).
Conclusion: The `newtype` strategy should not require the newtype constructor to be in scope. Instead, it should rely on the `Coercible` machinery to trigger the usual case where we need the constructor in scope. Of course, we should make sure that the error message is sensible when this happens.As I learned perusing !1916 (but you don't need to read that MR), `GeneralizedNewtypeDeriving` requires that the constructor of the newtype in question be in scope. Yet this isn't really necessary:
A.hs:
```hs
module A where
newtype N1 = MkN1 N2
newtype N2 = MkN2 N1
instance Eq N2 where
(==) = const (const False)
```
B.hs:
```hs
{# LANGUAGE DerivingStrategies, StandaloneDeriving, GeneralizedNewtypeDeriving,
DerivingVia #}
module B where
import A ( N1, N2(..) )
import Data.Coerce
 This fails:
 deriving newtype instance Eq N1
 This succeeds:
 deriving via N2 instance Eq N1
 This succeeds:
instance Eq N1 where
(==) = coerce ((==) :: N2 > N2 > Bool)
```
I would think that the three possible instance declarations in B.hs would all be completely equivalent. Yet the first is rejected while the last two are accepted.
This example is indeed silly, but it's possible to make mutuallyrecursive newtypes that are not silly (by using e.g. `Maybe` or `Either` to break the loop).
Conclusion: The `newtype` strategy should not require the newtype constructor to be in scope. Instead, it should rely on the `Coercible` machinery to trigger the usual case where we need the constructor in scope. Of course, we should make sure that the error message is sensible when this happens.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, 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 HEAD## 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/17323The Purely Kinded Type Invariant (PKTI) is not good enough20200124T11:45:59ZRichard Eisenbergrae@richarde.devThe Purely Kinded Type Invariant (PKTI) is not good enoughRequired reading: `Note [The Purely Kinded Type Invariant (PKTI)]` and `Note [mkAppTyM]`, both in TcHsType.
The PKTI has at least two problems.
1. Suppose we have the type `a > b` stored in `ty`. If we say `splitTyConApp ty`, we should expect to get `(funTyCon, [r1, r2, a, b])` where `a :: TYPE r1` and `b :: TYPE r2`. But what if `a` doesn't have type `TYPE r1` or `b` doesn't have type `TYPE r2`? This can happen if, say, `a :: kappa` and `kappa := TYPE r1`, but we haven't zonked. The PKTI must address this. This means that we will have to write `mkFunTyM` just like `mkAppTyM`. We might even need `mkTyConAppM` to handle the case when the tycon is `(>)`. :(
2. Nasty case 2 of `Note [mkAppTyM]` isn't sufficient. That case considers a type synonym. What about a type family?
```hs
type family F (a :: Type > Type) (b :: Type) where
F a b = a b
```
According to its current text of the PKTI, `F (a :: kappa1) (b :: kappa2)` satisfies the PKTI. Yet if we reduce this type family, `a b` does not satisfy the PKTI. Yet we sometimes reduce type families in a pure context (`normaliseType`) and, moreover, the main typefamilyreduction engine in TcFlatten does not respect the PKTI in this case as it does rewriting. (Actually, it does, because the flattener zonks thoroughly. But we're exploring the possibility of not zonking as thoroughly in the future. And, in any case, there is no documented connection between the flattener's desire to zonk and the PKTI.)
With some plumbing, etc., I'm confident we can fix (1). But I really have no idea how to fix (2). I worry we will have to abandon the idea of pure reductions, and we'll have to teach the flattener to check for "tricky tvs" (see `isTrickyTvBinder`) much like `mkAppTyM` does. Or, we can abandon pure reductions and just keep the flattener zonking thoroughly. :)Required reading: `Note [The Purely Kinded Type Invariant (PKTI)]` and `Note [mkAppTyM]`, both in TcHsType.
The PKTI has at least two problems.
1. Suppose we have the type `a > b` stored in `ty`. If we say `splitTyConApp ty`, we should expect to get `(funTyCon, [r1, r2, a, b])` where `a :: TYPE r1` and `b :: TYPE r2`. But what if `a` doesn't have type `TYPE r1` or `b` doesn't have type `TYPE r2`? This can happen if, say, `a :: kappa` and `kappa := TYPE r1`, but we haven't zonked. The PKTI must address this. This means that we will have to write `mkFunTyM` just like `mkAppTyM`. We might even need `mkTyConAppM` to handle the case when the tycon is `(>)`. :(
2. Nasty case 2 of `Note [mkAppTyM]` isn't sufficient. That case considers a type synonym. What about a type family?
```hs
type family F (a :: Type > Type) (b :: Type) where
F a b = a b
```
According to its current text of the PKTI, `F (a :: kappa1) (b :: kappa2)` satisfies the PKTI. Yet if we reduce this type family, `a b` does not satisfy the PKTI. Yet we sometimes reduce type families in a pure context (`normaliseType`) and, moreover, the main typefamilyreduction engine in TcFlatten does not respect the PKTI in this case as it does rewriting. (Actually, it does, because the flattener zonks thoroughly. But we're exploring the possibility of not zonking as thoroughly in the future. And, in any case, there is no documented connection between the flattener's desire to zonk and the PKTI.)
With some plumbing, etc., I'm confident we can fix (1). But I really have no idea how to fix (2). I worry we will have to abandon the idea of pure reductions, and we'll have to teach the flattener to check for "tricky tvs" (see `isTrickyTvBinder`) much like `mkAppTyM` does. Or, we can abandon pure reductions and just keep the flattener zonking thoroughly. :)https://gitlab.haskell.org/ghc/ghc//issues/17311Type family equality gets stuck on types that fail the occurs check20201211T15:47:16ZisovectorType family equality gets stuck on types that fail the occurs check## Summary
A type family that should check two types for equality gets stuck, even though their equality would fail the occurs check.
## Steps to reproduce
The following program doesn't compile:
```haskell
{# LANGUAGE AllowAmbiguousTypes #}
module Occurs where
import Data.Functor.Identity
import Data.Proxy
type family Equal a b where
Equal a a = 'True
Equal a b = 'False
foo :: Proxy (Equal (Identity a) a) > Proxy 'False
foo = id
```
with error:
```
• Couldn't match type ‘Equal (Identity a) a’ with ‘'False’
Expected type: Proxy (Equal (Identity a) a) > Proxy 'False
Actual type: Proxy 'False > Proxy 'False
• In the expression: id
In an equation for ‘foo’: foo = id
• Relevant bindings include
foo :: Proxy (Equal (Identity a) a) > Proxy 'False
(bound at /home/sandy/Vikrem.hs:14:1)

14  foo = id

```
The `Equal` type family is stuck due to `a` being a variable, but the only way `Equal (Identity a) a ~ 'True` is for an infinite instantiation of `a`. As such, this thing should reduce.
## Expected behavior
I expect the above program to compile, with `Equal (Identity a) a` reducing to `'False`.
## Environment
* GHC version used: 8.6.5
Optional:
* Operating System: Archlinux
* System Architecture: x86_64## Summary
A type family that should check two types for equality gets stuck, even though their equality would fail the occurs check.
## Steps to reproduce
The following program doesn't compile:
```haskell
{# LANGUAGE AllowAmbiguousTypes #}
module Occurs where
import Data.Functor.Identity
import Data.Proxy
type family Equal a b where
Equal a a = 'True
Equal a b = 'False
foo :: Proxy (Equal (Identity a) a) > Proxy 'False
foo = id
```
with error:
```
• Couldn't match type ‘Equal (Identity a) a’ with ‘'False’
Expected type: Proxy (Equal (Identity a) a) > Proxy 'False
Actual type: Proxy 'False > Proxy 'False
• In the expression: id
In an equation for ‘foo’: foo = id
• Relevant bindings include
foo :: Proxy (Equal (Identity a) a) > Proxy 'False
(bound at /home/sandy/Vikrem.hs:14:1)

14  foo = id

```
The `Equal` type family is stuck due to `a` being a variable, but the only way `Equal (Identity a) a ~ 'True` is for an infinite instantiation of `a`. As such, this thing should reduce.
## Expected behavior
I expect the above program to compile, with `Equal (Identity a) a` reducing to `'False`.
## Environment
* GHC version used: 8.6.5
Optional:
* Operating System: Archlinux
* System Architecture: x86_64https://gitlab.haskell.org/ghc/ghc//issues/17306:kind! should adhere to freductiondepth20191009T09:52:21ZJakob Brünker:kind! should adhere to freductiondepth## Summary
`:kind!` consumes gigabytes of memory for a while and then fails with `*** Exception: stack overflow` (GHCi itself does **not** crash, as long as enough memory is available) if given a nonterminating typelevel expression, while using such a type elsewhere will immediately result in ghc announcing that it has reached the limit of it's reduction stack (with size 200 by default, specified by `freductiondepth`). I can't be sure if this is intended, since `freductiondepth` doesn't appear to be documented in the user guide, but it's not something I would have expected.
## Steps to reproduce
Type the following in GHCi:
```haskell
:set XTypeFamilies XUndecidableInstances
type family F where F = F
:kind! F
```
Typing something like `undefined :: F` works as expected, with an error message about having reached a reduction stack size of 201.
## Expected behavior
I would expect to get the current error message from `undefined :: F` for both `undefined :: F` **and** `:kind! F`.
## Environment
* GHC version used:
8.6.5, 8.8.1, HEAD (8.9.0.20191001)
* Operating System:
Windows, nixos
* System Architecture:
x86_64## Summary
`:kind!` consumes gigabytes of memory for a while and then fails with `*** Exception: stack overflow` (GHCi itself does **not** crash, as long as enough memory is available) if given a nonterminating typelevel expression, while using such a type elsewhere will immediately result in ghc announcing that it has reached the limit of it's reduction stack (with size 200 by default, specified by `freductiondepth`). I can't be sure if this is intended, since `freductiondepth` doesn't appear to be documented in the user guide, but it's not something I would have expected.
## Steps to reproduce
Type the following in GHCi:
```haskell
:set XTypeFamilies XUndecidableInstances
type family F where F = F
:kind! F
```
Typing something like `undefined :: F` works as expected, with an error message about having reached a reduction stack size of 201.
## Expected behavior
I would expect to get the current error message from `undefined :: F` for both `undefined :: F` **and** `:kind! F`.
## Environment
* GHC version used:
8.6.5, 8.8.1, HEAD (8.9.0.20191001)
* Operating System:
Windows, nixos
* System Architecture:
x86_64