GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2022-03-15T22:16:55Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/18910Order-dependent type inference due to Note [Instance and Given overlap]2022-03-15T22:16:55ZRichard Eisenbergrae@richarde.devOrder-dependent type inference due to Note [Instance and Given overlap]With some effort, I have produced
```hs
{-# LANGUAGE ScopedTypeVariables, AllowAmbiguousTypes, TypeApplications,
TypeFamilies, PolyKinds, DataKinds, FlexibleInstances,
MultiParamTypeClasses, FlexibleContexts, P...With some effort, I have produced
```hs
{-# LANGUAGE ScopedTypeVariables, AllowAmbiguousTypes, TypeApplications,
TypeFamilies, PolyKinds, DataKinds, FlexibleInstances,
MultiParamTypeClasses, FlexibleContexts, PartialTypeSignatures #-}
module Bug where
import Data.Proxy
class P a
class Q a
class R a b
newtype Tagged (t :: k) a = Tagged a
type family F a
type instance F (Tagged @Bool t a) = [a]
instance P x => Q [x]
instance (x ~ y) => R y [x]
wob :: forall a b. (Q [b], R b a) => a -> Int
wob = undefined
it'sABoolNow :: forall (t :: Bool). Int
it'sABoolNow = undefined
class HasBoolKind t
instance k ~ Bool => HasBoolKind (t :: k)
it'sABoolLater :: forall t. HasBoolKind t => Int
it'sABoolLater = undefined
g :: forall t a. Q (F (Tagged t a)) => Proxy t -> [a] -> _
g _ x = it'sABoolNow @t + wob x
g2 :: forall t a. Q (F (Tagged t a)) => Proxy t -> [a] -> _
g2 _ x = wob x + it'sABoolNow @t
g3 :: forall t a. Q (F (Tagged t a)) => Proxy t -> [a] -> _
g3 _ x = it'sABoolLater @t + wob x
g4 :: forall t a. Q (F (Tagged t a)) => Proxy t -> [a] -> _
g4 _ x = wob x + it'sABoolLater @t
```
All of `g`, `g2`, and `g3` are accepted. `g4` is rejected. Note that `g4` is identical to `g3` except for changing the order of the summands.
What's going on:
Here is an excerpt from `Note [Instance and Given overlap]`:
```
Example, from the OutsideIn(X) paper:
instance P x => Q [x]
instance (x ~ y) => R y [x]
wob :: forall a b. (Q [b], R b a) => a -> Int
g :: forall a. Q [a] => [a] -> Int
g x = wob x
From 'g' we get the implication constraint:
forall a. Q [a] => (Q [beta], R beta [a])
If we react (Q [beta]) with its top-level axiom, we end up with a
(P beta), which we have no way of discharging. On the other hand,
if we react R beta [a] with the top-level we get (beta ~ a), which
is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
now solvable by the given Q [a].
```
Here is the scenario in the Note, when type-checking the Note's `g`:
```
[G] Q [a]
[W] Q [beta]
[W] R beta [a]
```
When we process the first Wanted, we might be tempted to use the instance, simplifying the Wanted to `P beta`. Doing this leads to failure. What we'd prefer is to recognize that the Given might be helpful later, and just to leave the Wanted as-is. Then, processing the `[W] R beta [a]` tells us that `beta ~ a`, and we go home happy.
The scenario in this ticket is rather more complicated. The instances are unchanged, but now we have a type family `F` in the mix. It all looks like
```
t :: kappa
[G] Q (F (Tagged @kappa t a))
[W] Q [beta]
[W] R beta [a]
```
The question is: when processing the first Wanted, should the Given block GHC from using the global instance? (Sidenote: I've used partial type signatures and polykinds here as a sneaky way of getting a metavariable into a Given. The partial type signature stops GHC from kind-generalizing the type, and thus `t`'s kind remains as `kappa` when processing the body.) If `kappa` is `Bool`, then the Given will eventually match and should block us from using the instance. If `kappa` is not `Bool`, then the Given will not apply. Yet in all of `g`..`g4`, `kappa` turns out to be `Bool`.
In `g`, we have `it'sABoolNow @t`, and the eager unifier sets `kappa := Bool` before the constraint solver gets a crack. The application of `F` reduces and the Given is recognized as relevant, blocking the use of the global instance.
In `g2`, the same happens.
In `g3`, we get a new `[W] HasBoolKind @kappa t`. This gets processed *before* the `Q [beta]` Wanted, and processing this sets `kappa := Bool`, leading the Given to reduce and block the use of the global instance.
In `g4`, however, the new `[W] HasBoolKind @kappa t` comes *after* the others. So we process `Q [beta]` *before* learning about `kappa`. The global instance is used, and we are left stuck with `[W] P a` that cannot be solved.
This all boils down to the `not (isFskTyVar tv)` check in `GHC.Tc.Solver.Monad.mightMatchLater`, which (effectively) says that type family applications in Givens match only themselves, not any arbitrary type. Removing that check fixes this problem. But it introduces another. The following program is accepted today:
```hs
{-# LANGUAGE TypeFamilies, FlexibleInstances, FlexibleContexts #-}
module Bug2 where
class C a where
meth :: a -> ()
instance C Int where
meth _ = ()
type family F a
foo :: C (F a) => a -> Int -> ()
foo _ n = meth n
```
If we strike that check from `mightMatchLater`, we get
```
• Overlapping instances for C Int arising from a use of ‘meth’
Matching instances:
instance C Int -- Defined at CbvOverlap.hs:10:10
There exists a (perhaps superclass) match:
from the context: C (F a)
bound by the type signature for:
foo :: forall a. C (F a) => a -> Int -> ()
at CbvOverlap.hs:15:1-32
(The choice depends on the instantiation of ‘’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
• In the expression: meth n
In an equation for ‘foo’: foo _ n = meth n
```
The (unrelated) `[G] C (F a)` blocks the useful `instance C Int`. Worse, the error message says that the overlap depends on the instantiation of <<empty list>>.
This new problem is not just theoretical. In my !4149 patch, I essentially made this change unintentionally, and GHC's Parser.hs stopped compiling (in stage 2), due to its `DisambECP` shenanigans. It's easy for me to replicate the current behavior, so my branch can continue, but this bug will remain.
I'm not sure what the solution is. If we allow type family applications in Givens to match any potential type, we will unavoidably cause the second bug. So perhaps the best course of action is to let sleeping dogs lie. Yet I was uncomfortable reinstating the old behavior, because it smelled off... and I wanted to understand it better. Thus this ticket.https://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/18875Occurs-check-y Givens rewrite once, but not twice2020-12-04T22:10:52ZRichard Eisenbergrae@richarde.devOccurs-check-y Givens rewrite once, but not twiceGHC remarkably accepts this program:
```hs
type family UnMaybe a where
UnMaybe (Maybe b) = b
class C c where
meth :: c
instance C (Maybe d) where
meth = Nothing
f :: (e ~ Maybe (UnMaybe e)) => e
f = meth
```
This is remarkable...GHC remarkably accepts this program:
```hs
type family UnMaybe a where
UnMaybe (Maybe b) = b
class C c where
meth :: c
instance C (Maybe d) where
meth = Nothing
f :: (e ~ Maybe (UnMaybe e)) => e
f = meth
```
This is remarkable because satisfying the `C e` constraint arising from the use of `meth` requires using the `e ~ Maybe (UnMaybe e)` given, despite the fact that it has an occurs-check failure. That is, GHC must rewrite `e` to `Maybe (UnMaybe e)` to solve the class constraint, yet not fall into a look trying to expand `e` further. This works due to the way GHC currently uses flattening-skolems to deal with type family applications. (The program above does not work on the current tip of !4149, which avoids this flattening mechanism.)
However, GHC rejects this program:
```hs
type family G a b where
G (Maybe c) d = d
h :: (e ~ Maybe (G e f)) => e -> f
h (Just x) = x
```
Here, `h` has a similar given with an occurs-check failure. In contrast to the first example, though, we need to use the equation *twice* in order to accept this program. Specifically, we have
```
[G] e ~ Maybe (G e f)
[W] e ~ Maybe f
```
Using the Given for rewriting once gives us
```
[W] Maybe (G e f) ~ Maybe f
```
which decomposes to
```
[W] G e f ~ f
```
But now, we must use the given *again* to get
```
[W] G (Maybe (G e f)) f ~ f
```
so that can reduce to
```
[W] f ~ f
```
and be solved.
I think this will be hard to achieve in practice (rewriting twice). Might we need even more rewrites in pathological scenarios? I don't know.
The purpose of this ticket is more to record the incompleteness than to actively agitate for a solution. This did not arise in a real application and would likely be hard to fix.https://gitlab.haskell.org/ghc/ghc/-/issues/18863Visibility mismatch between data declaration and kind signature, accepted!2023-09-27T08:24:13ZIcelandjackVisibility mismatch between data declaration and kind signature, accepted!```haskell
{-# Language PolyKinds #-}
{-# Language RankNTypes #-}
{-# Language StandaloneKindSignatures #-}
import Data.Kind
type ID :: forall i -> i -> Type
data ID :: forall i -> i -> Type
```
This compi...```haskell
{-# Language PolyKinds #-}
{-# Language RankNTypes #-}
{-# Language StandaloneKindSignatures #-}
import Data.Kind
type ID :: forall i -> i -> Type
data ID :: forall i -> i -> Type
```
This compiles on 8.10.0.20191123, if we change the standalone kind signature `forall->` to `forall.` we get an error. Obviously?
```haskell
-- • Couldn't match expected kind ‘forall i1 -> i1 -> *’
-- with actual kind ‘i -> *’
-- • In the data type declaration for ‘ID’
-- |
-- 8 | data ID :: forall i -> i -> Type
-- | ^^^^^^^
type ID :: forall i. i -> Type
data ID :: forall i -> i -> Type
```
But then why does this compile
```haskell
type ID :: forall i -> i -> Type
data ID :: forall i. i -> Type
```9.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/18802Typecheck record update via desugaring2022-05-26T07:45:30ZSimon Peyton JonesTypecheck record update via desugaringThere are quite a few tickets relating to inadequacies of record update, including
* #18311
* #10856
* #2595
* #10808
* #3632: updating existentials if you do all of them at once
* #16501
* #21289
* #21158
Record update is a place whe...There are quite a few tickets relating to inadequacies of record update, including
* #18311
* #10856
* #2595
* #10808
* #3632: updating existentials if you do all of them at once
* #16501
* #21289
* #21158
Record update is a place where our general plan of typechecking the source syntax seems particularly hard to do. It wold be much easier (and correct by construction) to desugar (but still in HsSyn) and typecheck that.
Fortunately we now have a way to do that: our [Re-engineer rebindable syntax](https://gitlab.haskell.org/ghc/ghc/-/issues/17582) ticket, #17582. A lot of attention is paid there to maintaining good error messages, which is the main challenge of this approach.
So this ticket is to propose: let's use the work on #17582 to solve our record-update tickets.
See also #21158 for why this will be a breaking change.9.6.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/18739Infer multiplicity of let expression2023-12-21T21:18:04ZArnaud SpiwackInfer multiplicity of let expression## Motivation
In a let expression `let x = rhs in u`, `x` is always bound with multiplicity `Many` (and, correspondingly, `u` is consumed with multiplicity `Many`).
This also holds of where expression `u where x = rhs`.
The situation ...## Motivation
In a let expression `let x = rhs in u`, `x` is always bound with multiplicity `Many` (and, correspondingly, `u` is consumed with multiplicity `Many`).
This also holds of where expression `u where x = rhs`.
The situation is similar to that of case expression as in #18738 .
In #18461 , we are adding a syntax to force polymorphism, but programmers expect let expressions to know their multiplicity on their own (in particular, they expect `let x = y in u` to be the same as `u[x\y]`, but if the latter consumes `y` linearly, the former never does in the current GHC).
## Proposal
Infer the multiplicity of `let` binders instead of choosing `Many` systematically. The multiplicity would be a variable.
A small detail to pay attention to is that, in `let pat = rhs in u`, the outermost pattern of `pat` is lazy. Lazy pattern are only permissible in unrestricted patterns (one way to think about it is that the desugaring of lazy pattern is not linear).
The typechecker doesn't make this property very apparent, so we will have to be careful about it. I suppose the same issue arises in #18461 .https://gitlab.haskell.org/ghc/ghc/-/issues/18738Infer multiplicity of case expression2022-11-25T10:42:33ZArnaud SpiwackInfer multiplicity of case expression## Motivation
As it stands, the following expression
```haskell
case u of {…}
```
is always understood by the typechecker as consuming `u` with multiplicity `Many`. This was done in the first iteration of patch in order to ensure bein...## Motivation
As it stands, the following expression
```haskell
case u of {…}
```
is always understood by the typechecker as consuming `u` with multiplicity `Many`. This was done in the first iteration of patch in order to ensure being fully compatible with regular Haskell without having to delve too much into inference issue.
This applies to case expressions and to pattern guards creating a pattern:
```haskell
| pat <- u, … = …
```
here u is also consumed with multiplicity `Many`.
(In a `\case` or a function definition by equations, the multiplicity is decided by the type that it is checked against, if any. So it may be any multiplicity.)
Core is already equipped to deal with arbitrary multiplicities here.
## Proposal
These expressions should infer the appropriate multiplicity. So typechecking such a case expression should emit a multiplicity variable instead of choosing `Many` systematically.
One somewhat subtle point to keep in mind is that some patterns require that the scrutinee be consumed unrestrictedly. That's the case, for instance, of wildcard patterns (`_`). I believe that the current implementation will handle a variable for the pattern's multiplicity smoothly (see `checkManyPattern` in `GHC.Tc.Gen.Pat` ([currently](https://gitlab.haskell.org/ghc/ghc/-/blob/d7385f7077c6258c2a76ae51b4ea80f6fa9c7015/compiler/GHC/Tc/Gen/Pat.hs#L348-349)). But it's worth double-checking.
For pattern guard the relevant code is the `BindStmt` case of `tcGuardStmt` in `GHC.Tc.Gen.Match`.
cc @monoidalhttps://gitlab.haskell.org/ghc/ghc/-/issues/18715ThBrackCtxt is unused2020-09-21T21:17:06ZRyan ScottThBrackCtxt is unusedThe [`UserTypeCtxt`](https://gitlab.haskell.org/ghc/ghc/-/blob/a1f34d37b47826e86343e368a5c00f1a4b1f2bce/compiler/GHC/Tc/Types/Origin.hs#L57-92) data type defines a context for TH brackets:
```hs
data UserTypeCtxt
= ...
| ThBrackCtxt...The [`UserTypeCtxt`](https://gitlab.haskell.org/ghc/ghc/-/blob/a1f34d37b47826e86343e368a5c00f1a4b1f2bce/compiler/GHC/Tc/Types/Origin.hs#L57-92) data type defines a context for TH brackets:
```hs
data UserTypeCtxt
= ...
| ThBrackCtxt -- Template Haskell type brackets [t| ... |]
| ...
```
However, this does not appear to actually be used anywhere and can be removed relatively easily:
<details>
```diff
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 3a1ab09c9b..e81a87c3a8 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -2831,7 +2831,6 @@ expectedKindInCtxt :: UserTypeCtxt -> ContextKind
-- Depending on the context, we might accept any kind (for instance, in a TH
-- splice), or only certain kinds (like in type signatures).
expectedKindInCtxt (TySynCtxt _) = AnyKind
-expectedKindInCtxt ThBrackCtxt = AnyKind
expectedKindInCtxt (GhciCtxt {}) = AnyKind
-- The types in a 'default' decl can have varying kinds
-- See Note [Extended defaults]" in GHC.Tc.Utils.Env
diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index b2fdefa4cd..cc63f7a5c5 100644
--- a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ -92,7 +92,6 @@ data UserTypeCtxt
-- True: stand-alone deriving
-- False: vanilla instance declaration
| SpecInstCtxt -- SPECIALISE instance pragma
- | ThBrackCtxt -- Template Haskell type brackets [t| ... |]
| GenSigCtxt -- Higher-rank or impredicative situations
-- e.g. (f e) where f has a higher-rank type
-- We might want to elaborate this
@@ -136,7 +135,6 @@ pprUserTypeCtxt (StandaloneKindSigCtxt n) = text "a standalone kind signature fo
pprUserTypeCtxt TypeAppCtxt = text "a type argument"
pprUserTypeCtxt (ConArgCtxt c) = text "the type of the constructor" <+> quotes (ppr c)
pprUserTypeCtxt (TySynCtxt c) = text "the RHS of the type synonym" <+> quotes (ppr c)
-pprUserTypeCtxt ThBrackCtxt = text "a Template Haskell quotation [t|...|]"
pprUserTypeCtxt PatSigCtxt = text "a pattern type signature"
pprUserTypeCtxt ResSigCtxt = text "a result type signature"
pprUserTypeCtxt (ForSigCtxt n) = text "the foreign declaration for" <+> quotes (ppr n)
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index fba45562b7..05dcb28643 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -372,7 +372,6 @@ checkValidType ctxt ty
ForSigCtxt _ -> rank1
SpecInstCtxt -> rank1
- ThBrackCtxt -> rank1
GhciCtxt {} -> ArbitraryRank
TyVarBndrKindCtxt _ -> rank0
@@ -500,7 +499,6 @@ vdqAllowed :: UserTypeCtxt -> Bool
vdqAllowed (KindSigCtxt {}) = True
vdqAllowed (StandaloneKindSigCtxt {}) = True
vdqAllowed (TySynCtxt {}) = True
-vdqAllowed (ThBrackCtxt {}) = True
vdqAllowed (GhciCtxt {}) = True
vdqAllowed (TyVarBndrKindCtxt {}) = True
vdqAllowed (DataKindCtxt {}) = True
@@ -1333,7 +1331,6 @@ okIPCtxt ResSigCtxt = True
okIPCtxt GenSigCtxt = True
okIPCtxt (ConArgCtxt {}) = True
okIPCtxt (ForSigCtxt {}) = True -- ??
-okIPCtxt ThBrackCtxt = True
okIPCtxt (GhciCtxt {}) = True
okIPCtxt SigmaCtxt = True
okIPCtxt (DataTyCtxt {}) = True
```
</details>
Is there a good reason to keep this around?https://gitlab.haskell.org/ghc/ghc/-/issues/18645Incremental `tcCheckSatisfiability` API2021-07-26T09:54:10ZSebastian GrafIncremental `tcCheckSatisfiability` APIThe pattern-match checker makes use of the function `tcCheckSatisfiability :: Bag EvVar -> TcM Bool` (henceforth `tcCS`) offered by the type-checker to solve type constraints. Over the course of a pattern-match checking session, such a `...The pattern-match checker makes use of the function `tcCheckSatisfiability :: Bag EvVar -> TcM Bool` (henceforth `tcCS`) offered by the type-checker to solve type constraints. Over the course of a pattern-match checking session, such a `Bag EvVar` is accumulated and incrementally checked after each addition. As #17836 shows in a rather painful way, that scales quadratically, because the type-checker chews through the same type constraints over and over again.
But look at how the pattern-match checker uses `tcCS`:
```hs
-- | Add some extra type constraints to the 'TyState'; return 'Nothing' if we
-- find a contradiction (e.g. @Int ~ Bool@).
tyOracle :: TyState -> Bag PredType -> DsM (Maybe TyState)
tyOracle (TySt inert) cts
= do { evs <- traverse nameTyCt cts
; let new_inert = inert `unionBags` evs
; ... <- initTcDsForSolver $ tcCheckSatisfiability new_inert
; ... }
```
The `inert` set is a `Bag EvVar` for which *we already know they are compatible with each other*, as they were checked by `tcCS` in a previous call. Only `cts :: Bag PredType` are unchecked. And as far as the pattern-match checker is concerned, the type of `inert` is completely opaque, so the API to `tcCS` could very well be
```hs
tcCheckSatisfiability :: TcInert -> Bag EvVar -> TcM (Maybe TcInert)
-- | Add some extra type constraints to the 'TyState'; return 'Nothing' if we
-- find a contradiction (e.g. @Int ~ Bool@).
tyOracle :: TyState -> Bag PredType -> DsM (Maybe TyState)
tyOracle (TySt inert) cts
= do { evs <- traverse nameTyCt cts
; ...mb_new_inert... <- initTcDsForSolver $ tcCheckSatisfiability inert evs
; ... }
```
I'm sure there already is something like `TcInert` in the type-checker. Looking at the implementation of `tcCS`, that might be the unused `EvBindMap`, but I'm not sure. Or is it the `InertCans` in `getInertCans`/`setInertCans`? CC @rae, @RyanGlScott, @simonpj
This blocks #17836 and would probably lead to quite a few (possibly rather drastic) metric decreases in other cases.https://gitlab.haskell.org/ghc/ghc/-/issues/18542Kind error when using partial type signatures2020-08-06T21:34:14Zlennart@augustsson.netKind error when using partial type signatures## Summary
When using a partial type signature I get a kind error, which is surprising.
## Steps to reproduce
Compile the following module. The function bar type checks, whereas baz gets a kind error
```
{-# LANGUAGE RankNTypes #-}...## Summary
When using a partial type signature I get a kind error, which is surprising.
## Steps to reproduce
Compile the following module. The function bar type checks, whereas baz gets a kind error
```
{-# LANGUAGE RankNTypes #-}
module Bug where
foo :: (Functor g) =>
(forall aa . Num aa => f aa -> g aa) ->
f a -> g (f a)
foo f x = undefined
bar :: (forall aa . Num aa => f aa -> Int -> aa) ->
f a -> Int -> f a
bar f = foo f
baz :: (forall aa . Num aa => f aa -> Int -> aa) ->
f a -> _ -> f a
baz f = foo f
```
## Environment
* GHC version used:
The Glorious Glasgow Haskell Compilation System, version 8.10.19.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/18481Improve instantiation of datacons2022-04-12T17:01:42ZKrzysztof GogolewskiImprove instantiation of dataconsThis ticket tracks a possible improvement to `return_data_con`.
When typechecking a datacon `T`, do we instantiate its arguments? We'd like to avoid instantiation, because it breaks VTA.
Currently, we instantiate levity-polymorphic con...This ticket tracks a possible improvement to `return_data_con`.
When typechecking a datacon `T`, do we instantiate its arguments? We'd like to avoid instantiation, because it breaks VTA.
Currently, we instantiate levity-polymorphic constructors. Quoting Note [Linear fields generalization]:
```
A small hitch: if the constructor is levity-polymorphic (unboxed tuples, sums,
certain newtypes with -XUnliftedNewtypes) then this strategy produces
\r1 r2 a b (x # p :: a) (y # q :: b) -> (# a, b #)
Which has type
forall r1 r2 a b. a #p-> b #q-> (# a, b #)
Which violates the levity-polymorphism restriction see Note [Levity polymorphism
checking] in DsMonad.
So we really must instantiate r1 and r2 rather than quantify over them. For
simplicity, we just instantiate the entire type, as described in Note
[Instantiating stupid theta]. It breaks visible type application with unboxed
tuples, sums and levity-polymorphic newtypes, but this doesn't appear to be used
anywhere.
A better plan: let's force all representation variable to be *inferred*, so that
they are not subject to visible type applications. Then we can instantiate
inferred argument eagerly.
```
The goal of this ticket is to implement the last paragraph.https://gitlab.haskell.org/ghc/ghc/-/issues/18451Infinite loop during kind inference2020-07-27T08:10:18ZSimon Peyton JonesInfinite loop during kind inferenceThis program
```
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
type Const a b = a
data SameKind :: k -> k -> Type
type T (k :: Const Type a) = forall (b :: k). SameKind a b
```
goes into an ...This program
```
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
type Const a b = a
data SameKind :: k -> k -> Type
type T (k :: Const Type a) = forall (b :: k). SameKind a b
```
goes into an infinite loop during kind checking. (Extracted from #16245.)
We have
```
a_agk :: k_au5
k_atM :: Const Type a_agk
k_au5 := k_au7
```
and then we try to unify `k_au7 := k_atM`. That should be an occurs-check error, since `k_atM`'s kind mentions `a_agk`, whose kind mentions `k_au5`, which is equal to `k_au7`.
But `occCheckExpand` (called from `GHC.Tc.Utils.Unify.metaTyVarUpdateOK`) expands the `Const` synonym in `k_atM`'s kind so that it no longer mentions `a_agk`, which allows the update to go ahead.
Wrong! We can't do this `occCheckExpand` business inside kinds! Let's just not do that.https://gitlab.haskell.org/ghc/ghc/-/issues/18439Pattern guards can break linearity2021-01-08T16:49:06ZArnaud SpiwackPattern guards can break linearity## Summary
Patterns, in pattern-guards guards are not checked for linearity. Which let's us write incorrect program with respect to linearity. The linter rightfully rejects those.
## Steps to reproduce
This typechecks but should not:
...## Summary
Patterns, in pattern-guards guards are not checked for linearity. Which let's us write incorrect program with respect to linearity. The linter rightfully rejects those.
## Steps to reproduce
This typechecks but should not:
```
{-# LANGUAGE LinearTypes #-}
unsafeConsume :: a #-> ()
unsafeConsume x | _ <- x = ()
```
## Environment
* GHC version used: master 3656dff8259199d0dab2d1a1f1b887c252a9c1a3
## Note
Originally reported by Roman Cheplyaka.Arnaud SpiwackArnaud Spiwackhttps://gitlab.haskell.org/ghc/ghc/-/issues/18412Monotype check for case branches should not recur through arrows2020-07-20T07:57:36ZRichard Eisenbergrae@richarde.devMonotype check for case branches should not recur through arrowsConsider this module:
```hs
{-# LANGUAGE RankNTypes #-}
module Bug where
hr :: (forall a. a -> a) -> ()
hr _ = ()
foo x = case x of () -> hr
bar x = case x of True -> hr
False -> hr
```
On HEAD, `foo` is accepted ...Consider this module:
```hs
{-# LANGUAGE RankNTypes #-}
module Bug where
hr :: (forall a. a -> a) -> ()
hr _ = ()
foo x = case x of () -> hr
bar x = case x of True -> hr
False -> hr
```
On HEAD, `foo` is accepted while `bar` is rejected. (This is not a change from previous behavior.) The reason is that GHC requires `case` branches (when there are more than 1; and when the result of the `case` is being inferred, not checked) to have monotypes, lest it be left with the task of finding the most general supertype of a bunch of polytypes. However, now that we have simplified subsumption, it is draconian to propagate the monotype check past arrows. I thus claim that `bar` should be accepted.https://gitlab.haskell.org/ghc/ghc/-/issues/18406Functional dependency should constrain local inferred type, but does not2022-02-23T13:21:42ZRichard Eisenbergrae@richarde.devFunctional dependency should constrain local inferred type, but does notIf I compile
```hs
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
module Bug where
class C a b | a -> b where
op :: a -> a
foo :: C a b => a -> b -> a
foo x y = blah x
where
blah z = [x,z] `seq` op z
```
with...If I compile
```hs
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
module Bug where
class C a b | a -> b where
op :: a -> a
foo :: C a b => a -> b -> a
foo x y = blah x
where
blah z = [x,z] `seq` op z
```
with `-ddump-tc -fprint-typechecker-elaboration -fprint-explicit-foralls`, I get
```
==================== Typechecker ====================
AbsBinds [a_apDT, b_apDU] [$dC_apDW]
{Exports: [foo <= foo_apDV
wrap: <>]
Exported types: foo :: forall a b. C a b => a -> b -> a
[LclId]
Binds: foo_apDV x_apD6 y_apD7
= blah_apD8 @ b_apDU $dC_apEm x_apD6
where
AbsBinds [b_apE7] [$dC_apEd]
{Exports: [blah_apD8 <= blah_apEb
wrap: <>]
Exported types: blah_apD8
:: forall {b}. C a_apDT b => a_apDT -> a_apDT
[LclId]
Binds: blah_apD8 z_apD9
= [x_apD6, z_apD9] `seq` op @ a_apDT @ b_apE7 $dC_apE8 z_apD9
Evidence: [EvBinds{[W] $dC_apE8 = $dC_apEd}]}
Evidence: [EvBinds{[W] $dC_apEm = $dC_apDW}]}
```
Note that the local `blah` gets type `forall {b}. C a b => a -> a`. Why quantify `b` locally? There is no reason to. There is no great harm either, but a patch I'm working on (https://gitlab.haskell.org/ghc/ghc/-/tree/wip/derived-refactor) gets annoyed when this condition (which happens in the wild, in `Text.Parsec.Perm`) causes `[G] C a b1` and `[G] C a b2` to both be in scope with no relationship between `b1` and `b2`.
Will fix in ongoing work.https://gitlab.haskell.org/ghc/ghc/-/issues/18311Record update is over-restrictive2022-05-26T07:40:34ZSimon Peyton JonesRecord update is over-restrictiveConsider
```
type family F a
type instance F Int = Int
type instance F Bool = Int
data T a = MkT { x :: F a, y :: a }
foo1 :: T Int -> T Bool
foo1 (MkT { x = x }) = MkT { x = x, y = True}
foo2 :: T Int -> T Bool
foo2 t = t { y = True...Consider
```
type family F a
type instance F Int = Int
type instance F Bool = Int
data T a = MkT { x :: F a, y :: a }
foo1 :: T Int -> T Bool
foo1 (MkT { x = x }) = MkT { x = x, y = True}
foo2 :: T Int -> T Bool
foo2 t = t { y = True }
```
`foo1` typechecks fine, but `foo2` complains
```
Foo.hs:16:10: error:
• Couldn't match type ‘Int’ with ‘Bool’
Expected type: T Bool
Actual type: T Int
• In the expression: t {y = True}
In an equation for ‘foo2’: foo2 t = t {y = True}
```
This is bogus. `foo2` should be fine -- precisely because `foo1` is.
The offending code is in the `RecordUpd` case of `GHc.Tc.Gen.Expr.tcExpr`. See this comment
```
-- STEP 4 Note [Type of a record update]
-- Figure out types for the scrutinee and result
-- Both are of form (T a b c), with fresh type variables, but with
-- common variables where the scrutinee and result must have the same type
-- These are variables that appear in *any* arg of *any* of the
-- relevant constructors *except* in the updated fields
```
With the advent of type families "appearing in" a type is not the same as being fixed by it.
Not hard to fix; might even lead to less code!https://gitlab.haskell.org/ghc/ghc/-/issues/18300UnliftedNewtypesDifficultUnification broken due to simplified subsumption2020-07-03T21:33:23ZBen GamariUnliftedNewtypesDifficultUnification broken due to simplified subsumption`UnliftedNewtypesDifficultUnification` fails due to simplified subsumption patch (!2600) in `DEBUG`-enabled compiler.
```
Compile failed (exit code 1) errors were:
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.11.0.202...`UnliftedNewtypesDifficultUnification` fails due to simplified subsumption patch (!2600) in `DEBUG`-enabled compiler.
```
Compile failed (exit code 1) errors were:
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.11.0.20200603:
ASSERT failed! file compiler/GHC/Core/FamInstEnv.hs, line 651
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
*** unexpected failure for UnliftedNewtypesDifficultUnification(normal)
```
I have marked this test as broken in the interest of getting !2600 merged.
As seen in Job [#356282](https://gitlab.haskell.org/ghc/ghc/-/jobs/356282).9.0.1Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/18151Eta-expansion of a left-section2021-01-12T23:04:49ZRichard Eisenbergrae@richarde.devEta-expansion of a left-sectionIf I say
```hs
x = seq (True `undefined`) ()
```
what should I get when evaluating `x`?
According to my understanding of the Haskell Report, I should get `()`. And according to my understanding of GHC's source code (in `GHC.Tc.Gen.Exp...If I say
```hs
x = seq (True `undefined`) ()
```
what should I get when evaluating `x`?
According to my understanding of the Haskell Report, I should get `()`. And according to my understanding of GHC's source code (in `GHC.Tc.Gen.Expr`), I should get `()`. But I get an exception.
Why?
NB: `-XPostfixOperators` is off. If it were on, the exception would be expected.
Spun off from https://github.com/ghc-proposals/ghc-proposals/pull/275#issuecomment-6242820229.0.1Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc/-/issues/18073Out-of-date commentary in Tc.Deriv.Infer2020-04-23T03:49:06ZRichard Eisenbergrae@richarde.devOut-of-date commentary in Tc.Deriv.InferCheck out https://gitlab.haskell.org/ghc/ghc/-/blob/15ab6cd548f284732a7f89d78c2b89b1bfc4ea1d/compiler/GHC/Tc/Deriv/Infer.hs#L805
* The commentary there talks about creating a variable `unsolved`, which does not seem to exist.
* In addi...Check out https://gitlab.haskell.org/ghc/ghc/-/blob/15ab6cd548f284732a7f89d78c2b89b1bfc4ea1d/compiler/GHC/Tc/Deriv/Infer.hs#L805
* The commentary there talks about creating a variable `unsolved`, which does not seem to exist.
* In addition, the partition below creates `bad`, which is just ignored. Maybe this is right -- I have not thought about it. But if it is right, it should be documented.
cc @RyanGlScott