GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2020-07-17T13:59:54Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/18456"equirecursive" type family leads to stack overflow in ghci2020-07-17T13:59:54ZXia Li-yao"equirecursive" type family leads to stack overflow in ghci## Summary
Trying to typecheck a term using a (silly) type family such that `T ~ Maybe T` leads to a stack overflow (instead of a proper type error from reaching the max reduction depth, if this is to be an error at all).
## Steps to r...## Summary
Trying to typecheck a term using a (silly) type family such that `T ~ Maybe T` leads to a stack overflow (instead of a proper type error from reaching the max reduction depth, if this is to be an error at all).
## Steps to reproduce
```
> :set -XTypeFamilies -XUndecidableInstances
> type family T where T = Maybe T
> :t Nothing @T
Nothing @T*** Exception: stack overflow
```
(where the exception takes a few seconds to appear)
Compare that output to this variant that immediately produces a proper type error:
```
> :t Nothing @T :: T
<interactive>:5:1 error:
...
```
## Expected behavior
Either a success (`Nothing @T` has type `Maybe T` without requiring any type conversion), or a type error instead of an internal exception.
## Environment
* GHC version used: 8.10.1https://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/18413Suboptimal constraint solving2021-09-06T08:27:32ZSimon Peyton JonesSuboptimal constraint solvingHere a summary of `-ddump-tc-trace` for this program (part of test T12427a)
```
data T where
T1 :: a -> ((forall b. [b]->[b]) -> Int) -> T
h11 y = case y of T1 _ v -> v
```
I see this sequence
```
{co_awA} {0}:: ((forall b. [b] -> [...Here a summary of `-ddump-tc-trace` for this program (part of test T12427a)
```
data T where
T1 :: a -> ((forall b. [b]->[b]) -> Int) -> T
h11 y = case y of T1 _ v -> v
```
I see this sequence
```
{co_awA} {0}:: ((forall b. [b] -> [b]) -> Int)
~# p_awz[tau:1] (CNonCanonical)
==> Hetero equality gives rise to kind equality
inert: {co_awG} :: p_awz[tau:1] ~# ((forall b. [b] -> [b]) -> Int |> (TYPE {co_awF})_N)
work item: {co_awF} :: 'GHC.Types.LiftedRep ~# p_awy[tau:1]
co_awA := Sym ({co_awG} ; Sym (GRefl nominal ((forall b.[b] -> [b]) -> Int)
(TYPE {co_awF})_N))
==> Swap awF, kick out awG
work item: {co_awG} :: p_awz[tau:1] ~# ((forall b. [b] -> [b]) -> Int |> (TYPE {co_awF})_N)
inert (because p_awy is untouchable):
{co_awH} :: p_awy[tau:1] ~# 'GHC.Types.LiftedRep
co_awF := Sym co_awH
==> flatten awG (strange double GRefl)
inert: {co_awH} :: p_awy[tau:1] ~# 'GHC.Types.LiftedRep
inert: {co_awI} :: p_awz[tau:1] ~# ((forall b. [b] -> [b]) -> Int |> (TYPE (Sym {co_awH}))_N)
co_awG := {co_awI} ; (Sym (GRefl nominal ((forall b. [b] -> [b]) -> Int)
(TYPE (Sym {co_awH}))_N)
; GRefl nominal ((forall b. [b] -> [b]) -> Int)
(TYPE {co_awF})_N)
at this point we also make a derived shadow of awI, for some reason.
Solving stops here, but we float out awI, and awH, and then have another go
work: {co_awH} :: p_awy[tau:1] ~# 'GHC.Types.LiftedRep
work: {co_awI} :: p_awz[tau:1] ~# ((forall b. [b] -> [b]) -> Int |> (TYPE (Sym {co_awH}))_N)
==> flatten awI (why?)
work: {co_awH} :: p_awy[tau:1] ~# 'GHC.Types.LiftedRep
inert: {co_awJ} :: p_awz[tau:1] ~# ((forall b. [b] -> [b]) -> Int |> (TYPE (Sym {co_awH}))_N)
co_awI := {co_awJ} ; (Sym (GRefl nominal ((forall b. [b] -> [b]) -> Int)
(TYPE (Sym {co_awH}))_N) ; GRefl nominal ((forall b. [b] -> [b])
-> Int)
(TYPE (Sym {co_awH}))_N)
==> solve awH: p_awy := LiftedRep, kick out awJ
{co_awJ} :: p_awz[tau:1] ~# ((forall b. [b] -> [b]) -> Int |> (TYPE (Sym {co_awH}))_N)
==> flatten awJ
co_awJ := {co_awK} ; GRefl nominal ((forall b. [b] -> [b]) -> Int)
(TYPE (Sym {co_awH}))_N
{co_awK} :: p_awz[tau:1] ~# ((forall b. [b] -> [b]) -> Int)
```
This seems like we are doing too much work, esp the double GRefls. Why did awI get flattened?
It's not a disaster, but pretty heavy handed.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://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/18308Order of StandaloneKindSignatures and CUSKs extensions significant2021-03-31T15:14:45ZBjörn HegerforsOrder of StandaloneKindSignatures and CUSKs extensions significant## Summary
I have some code that compiles without the `StandaloneKindSignatures` extension, does not compile with it, but does compile again if I also add the `CUSKs` extension _after_ `StandaloneKindSignatures`. However, if I place the...## Summary
I have some code that compiles without the `StandaloneKindSignatures` extension, does not compile with it, but does compile again if I also add the `CUSKs` extension _after_ `StandaloneKindSignatures`. However, if I place the `CUSKs` extension _before_ `StandaloneKindSignatures`, then the code doesn't compile.
I'm not sure if I can avoid a CUSK in this case either, because it revolves around an associated type family, which to my understanding stand-alone kind signatures cannot (yet) be written for.
I generally try to keep my extensions arranged alphabetically, which is unfortunate in this case. But that's not at all a big worry. For now I can put `CUSKs` after `StandaloneKindSignatures` as a workaround.
## Steps to reproduce
Boiling it down to a minimal demonstrative case, this compiles:
```haskell
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE CUSKs #-}
import Data.Kind (Type)
import Data.Proxy (Proxy)
class Cls where
type Fam (k :: Type) (a :: k) :: Type
mtd :: Proxy k -> Proxy (a :: k) -> Fam k a -> Int
```
but this doesn't:
```haskell
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE CUSKs #-}
{-# LANGUAGE StandaloneKindSignatures #-}
import Data.Kind (Type)
import Data.Proxy (Proxy)
class Cls where
type Fam (k :: Type) (a :: k) :: Type
mtd :: Proxy k -> Proxy (a :: k) -> Fam k a -> Int
```
## Expected behavior
I would expect both of the above to compile.
I should also note that it's not very clear to me what it is about the type signature for `mtd` that makes it problematic. The part that is sensitive here is the `(a :: k)` kind annotation. Whether I instead put that annotation in a `forall` makes no difference. If I simply remove the kind annotation for `a`, and let it be inferred, the code compiles regardless of which of `StandaloneKindSignatures` and `CUSKs` are enabled (and in which order). I don't know if this part behaves as expected or not.
## Environment
* GHC version used: 8.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/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/18295Outdated commentary in solveNestedImplications?2020-06-04T15:36:21ZRichard Eisenbergrae@richarde.devOutdated commentary in solveNestedImplications?`GHC.Tc.Solver.solveNestedImplications` looks like this:
```hs
solveNestedImplications :: Bag Implication
-> TcS (Cts, Bag Implication)
-- Precondition: the TcS inerts may contain unsolved simples which have
-- t...`GHC.Tc.Solver.solveNestedImplications` looks like this:
```hs
solveNestedImplications :: Bag Implication
-> TcS (Cts, Bag Implication)
-- Precondition: the TcS inerts may contain unsolved simples which have
-- to be converted to givens before we go inside a nested implication.
solveNestedImplications implics
| isEmptyBag implics
= return (emptyBag, emptyBag)
| otherwise
= do { traceTcS "solveNestedImplications starting {" empty
; (floated_eqs_s, unsolved_implics) <- mapAndUnzipBagM solveImplication implics
; let floated_eqs = concatBag floated_eqs_s
-- ... and we are back in the original TcS inerts
-- Notice that the original includes the _insoluble_simples so it was safe to ignore
-- them in the beginning of this function.
; traceTcS "solveNestedImplications end }" $
vcat [ text "all floated_eqs =" <+> ppr floated_eqs
, text "unsolved_implics =" <+> ppr unsolved_implics ]
; return (floated_eqs, catBagMaybes unsolved_implics) }
```
I believe that both the `Precondition:` and the `... and we are back` comments are out of date. If they are not, they should be clarified, as I have no idea what they mean.
Also:
```hs
solveImplication :: Implication -- Wanted
-> TcS (Cts, -- All wanted or derived floated equalities: var = type
Maybe Implication) -- Simplified implication (empty or singleton)
-- Precondition: The TcS monad contains an empty worklist and given-only inerts
-- which after trying to solve this implication we must restore to their original value
```
The empty-worklist precondition seems reasonable, but the "given-only inerts" bit is as mysterious as (and sounds quite related to) the previous problem.
@simonpj help?https://gitlab.haskell.org/ghc/ghc/-/issues/18220Improve Coercible under foralls2020-05-22T23:36:26ZSimon Peyton JonesImprove Coercible under forallsConsider
```
newtype Age = MkAge Int
h :: forall m. m Int -> m Age
h x = coerce @(m Int) @(m Age) x
```
This fails, as it should, with
```
Couldn't match representation of type 'm Int'
with that o...Consider
```
newtype Age = MkAge Int
h :: forall m. m Int -> m Age
h x = coerce @(m Int) @(m Age) x
```
This fails, as it should, with
```
Couldn't match representation of type 'm Int'
with that of 'm Age'
arising from a use of 'coerce'
NB: We cannot know what roles the parameters to 'm' have;
we must assume that the role is nominal
```
And indeed, if we have
```
type family F a
data T a = MkT (F a)
```
Then `h @T` would indeed be bogus because `T Int` and `T Age` might have very different representations.
So far so good. Now consider
```
f :: forall m. (forall p q. Coercible p q => Coercible (m p) (m q))
=> m Int -> m Age
f x = coerce @(m Int) @(m Age) x
g :: forall m. (forall p q. Coercible p q => Coercible (m p) (m q))
=> (forall a. a -> m Int) -> (forall a. a-> m Age)
g x = coerce @(forall a. a -> m Int) @(forall a. a -> m Age) x
```
Here `f` succeeds. It needs `[W] Coercible (m Int) (m Age)` which it can prove from the quantified constraint.
But `g` is rejected with
```
Couldn't match representation of type 'm Int'
with that of 'm Age'
arising from a use of 'coerce'
NB: We cannot know what roles the parameters to 'm' have;
we must assume that the role is nominal
In the expression:
coerce @(forall a. a -> m Int) @(forall a. a -> m Age) x
```
That's odd! I can easily come up with a succesful elaboration of the program. Why? We start from
```
[W] Coercible (forall a. a -> m Int) (forall a. a -> m Age)
===>
[W] (forall a. a -> m Int) ~R# (forall a. a -> m Age)
===> {make an implication constraint}
[W] forall <noev> a. () => (a -> m Int) ~R# (a -> m Age)
```
The `<noev>` says that we don't have a place to put value-level evidence. Then we decompose:
```
===>
[W] forall <noev> a. () => (m Int) ~R# (m Age)
```
and now we are stuck because there is nowhere to put the evidence.
But the solution is simple! Just float the constraint out of the implication (it does not mention the skolem `a`). I have done this in !3319, and indeed it works.
However, it doesn't solve the full problem. What we wanted `m a Int ~R# m a Age`? Now the skolem `a` would prevent the constraint floating out, and we are back to square 1
---------------------------------
That term-level quantified constraint `(forall p q. Coercible p q => Coercible (m p) (m q))` is really a way of saying "m's first argument has representational role". Perhaps we should seek a way of saying that more directly, and in a way we can use in coercions. Something like `Rep# m`. Then the evidence for `Rep# m` justifies decomposing a wanted constraint `m t1 ~R# m t2`.
Another alternative would be to decorate the arrow in m's kind, as we proposed in the first roles paper.
Neither seems simple. So this ticket is just recording the issue, and pointing to the MR, for posterity.
-------------
All this arose in #18148 and #18213, but is only tangentially related in the end.https://gitlab.haskell.org/ghc/ghc/-/issues/18196Type synonym lost with GADTs2021-10-17T13:38:04ZIdentical SnowflakeType synonym lost with GADTsConsider the following:
```haskell
type Joules = Double
type Grams = Double
data Unit a where
Energy :: Unit Joules
Mass :: Unit Grams
test :: Unit a -> a
test Energy = _
```
GHC reports the hole as `_ :: Double`, but I expected ...Consider the following:
```haskell
type Joules = Double
type Grams = Double
data Unit a where
Energy :: Unit Joules
Mass :: Unit Grams
test :: Unit a -> a
test Energy = _
```
GHC reports the hole as `_ :: Double`, but I expected the synonym to remain intact, i.e., that the hole would be `_ :: Joules`.https://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 @RyanGlScotthttps://gitlab.haskell.org/ghc/ghc/-/issues/18062A cast might get in the way of instantiation2020-04-27T10:20:56ZSimon Peyton JonesA cast might get in the way of instantiationSuppose we have a type signature `f :: forall a. Eq a => blah`, and it somehow kind-checks to
```
forall a. ((Eq a => Blah) |> co)
```
In principle this can happen:
```
tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) ...Suppose we have a type signature `f :: forall a. Eq a => blah`, and it somehow kind-checks to
```
forall a. ((Eq a => Blah) |> co)
```
In principle this can happen:
```
tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind
= do { ctxt' <- tc_hs_context mode ctxt
; ek <- newOpenTypeKind -- The body kind (result of the function) can
-- be TYPE r, for any r, hence newOpenTypeKind
; ty' <- tc_lhs_type mode rn_ty ek
; checkExpectedKind (unLoc rn_ty) (mkPhiTy ctxt' ty')
liftedTypeKind exp_kind }
```
That `checkExpectedKind` can add a cast.
If this happens, our instantiation mechanisms would fall over in a heap. We'd instantiate the `forall a`, but then fail to instantiate the `Eq a =>`; instead we'd unify `(Eq a => blah) |> co` with the function body. Bad, bad.
This popped up when fixing #18008, when a missing zonk in `tcHsPartialSigType` was producing just such a forall (with a Refl coercion). But it seems plausible that it could happen for real.
EDIT: And it does:
```hs
{-# LANGUAGE KindSignatures, TypeFamilies, DataKinds #-}
module Bug where
import Data.Kind ( Type )
type family Star where
Star = Type
f :: ((Eq a => a -> Bool) :: Star)
f x = x == x
```
produces
```
Bug.hs:11:1: error:
• Couldn't match kind ‘Constraint’ with ‘*’
When matching types
a0 :: *
Eq a :: Constraint
Expected type: Eq a => a -> Bool
Actual type: a0 -> Bool
• The equation(s) for ‘f’ have one argument,
but its type ‘Eq a => a -> Bool’ has none
• Relevant bindings include
f :: Eq a => a -> Bool (bound at Bug.hs:11:1)
|
11 | f x = x == x
| ^^^^^^^^^^^^
```
Solution: teach instantiation to look through casts.https://gitlab.haskell.org/ghc/ghc/-/issues/18007GHCi infers too-general type when pattern-matching on existential GADT2022-09-06T11:38:59Zinfinity0GHCi infers too-general type when pattern-matching on existential GADTRun the following in ghci, I tested with version 8.8.3:
<summary>
`ghci -ghci-script Test.hs`
<details>
```haskell
:set -XGADTs
:set -XScopedTypeVariables
-- standard GADT with restricted type param
data X a where X :: X Int; XB :: ...Run the following in ghci, I tested with version 8.8.3:
<summary>
`ghci -ghci-script Test.hs`
<details>
```haskell
:set -XGADTs
:set -XScopedTypeVariables
-- standard GADT with restricted type param
data X a where X :: X Int; XB :: X Bool
-- =============================================================================
-- standard ADT with full type params
data Pair0 a b t = Pair0 (a t) (b t)
Pair0 X x <- pure (Pair0 X [])
:t x
-- x :: [Int] as expected
x /= [10]
-- True
-- as expected, type inference matches x with [10]
-- =============================================================================
-- existential ADT, same as DSum from Data.Dependent.Sum
data Pair a b = forall t. Pair (a t) (b t)
-- same results with this equivalent GADT-syntax definition:
-- data Pair a b where Pair :: a t -> b t -> Pair a b
Pair X x <- pure (Pair X [])
x /= [10]
-- somehow, type inference fails to match x with [10]
-- • Couldn't match expected type ‘x’ with actual type ‘Integer’
:t x
-- x :: [t] but it should be
-- x :: [Int] because of the Pair X
--------------------------------------------------------------------------------
Pair X (x :: [Int]) <- pure (Pair X [])
x /= [10]
-- True
-- giving an explicit type signature fixes inference
--------------------------------------------------------------------------------
Pair X x <- pure (Pair X [0])
x /= [10]
-- True
-- giving an explicit value [0] also fixes inference
--------------------------------------------------------------------------------
:{
test :: IO ()
test = do
Pair X x <- pure (Pair X [])
print (x /= [10])
:}
test
-- True
-- putting the code inside a function, also fixes inference??
:{
test1 :: IO (Pair X [])
test1 = pure (Pair X [])
test2 :: Pair X [] -> IO ()
test2 (Pair X x) = print (x /= [10])
:}
test1 >>= test2
-- True
-- separating the functions also works, and we never hint x's type
```
</details>
</summary>
I think this is different from #2206 and #14065 since the error message here is a pretty generic "Couldn't match type" rather than the GADT-specific error messages in those tickets ("GADT pattern match with non-rigid result type", "untouchable inside the constraints"), and it only affects GHCi.https://gitlab.haskell.org/ghc/ghc/-/issues/17955mkNewTyConRhs panic when trying to constrain newtype with Coercible2021-01-23T06:44:33ZmatzemathicsmkNewTyConRhs panic when trying to constrain newtype with Coercible## Summary
The following code panics in ghc 8.8.3:
```haskell
{-# LANGUAGE FlexibleContexts #-}
import Data.Coerce
newtype T = Coercible () T => T ()
```
Error message:
```
[1 of 1] Compiling Main ( abug.hs, abug.o )
gh...## Summary
The following code panics in ghc 8.8.3:
```haskell
{-# LANGUAGE FlexibleContexts #-}
import Data.Coerce
newtype T = Coercible () T => T ()
```
Error message:
```
[1 of 1] Compiling Main ( abug.hs, abug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.8.3 for x86_64-unknown-linux):
mkNewTyConRhs
T [Coercible () T, ()]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
pprPanic, called at compiler/iface/BuildTyCl.hs:65:27 in ghc:BuildTyCl
```
This seems to come from whatever is done to infer Coercible's instances.
Any other Constraint (weather or not using a multi parameter class) gives an error message:
```haskell
{-# LANGUAGE FlexibleContexts #-}
newtype T = Show T => T ()
```
results in:
```
[1 of 1] Compiling Main ( abug.hs, abug.o )
abug.hs:3:13: error:
* A newtype constructor cannot have a context in its type
T :: Show T => () -> T
* In the definition of data constructor `T'
In the newtype declaration for `T'
|
3 | newtype T = Show T => T ()
| ^^^^^^^^^^^^^^
```
## Expected behavior
Should most likely print an error message as in the second example.
## Environment
* GHC version used: 8.8.39.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/17934Consider using specificity to disambiguate quantified constraints2021-02-21T15:37:18ZRichard Eisenbergrae@richarde.devConsider using specificity to disambiguate quantified constraints**Summary:** Currently, quantified constraints shadow global instances. This ticket proposes to use specificity (in the sense used by overlapping instances) instead of shadowing.
**Motivation**
This looks like a sensible way of having ...**Summary:** Currently, quantified constraints shadow global instances. This ticket proposes to use specificity (in the sense used by overlapping instances) instead of shadowing.
**Motivation**
This looks like a sensible way of having a datatype that can store something of a type that supports some class interface:
```haskell
data Some (c :: Type -> Constraint) where
Some :: c a => a -> Some c
```
But now I want to write a `Show` instance. I can do this only when the existential `a` supports `Show`. But I don't wish to require that `c ~ Show` -- maybe `c a` implies `Show a`. So I write this:
```haskell
instance (forall x . c x => Show x) => Show (Some c) where
showsPrec n (Some a) = showsPrec n a
```
But now this fails. The problem is that the instance gets expanded to
```haskell
instance (forall x . c x => Show x) => Show (Some c) where
showsPrec n (Some a) = showsPrec n a
show = $dmshow
```
where `$dmshow :: Show a => a -> String` is the default method implementation for `show`. When type-checking this method, GHC needs to satisfy `Show (Some c)`. The context includes two possibilities: the quantified constraint, and the top-level instance declaration. Because local instances (= quantified constraints) shadow global ones, we use the first. So we reduce `[W] Show (Some c)` to `[W] c (Some c)`, which cannot be solved, leading to disaster.
This example first came to light in https://gitlab.haskell.org/ghc/ghc/issues/16502#note_253501, where it was copied from #17794.
Taking this new approach will likely fix #16502 and allow the original program in #17202 to be accepted. See also https://gitlab.haskell.org/ghc/ghc/issues/16502#note_253501 and https://gitlab.haskell.org/ghc/ghc/issues/16502#note_259055 for more test cases.
**Background**:
The current instance lookup (as documented [here](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#instance-lookup)) works as follows to solve a `[W] C T` constraint (for some class `C` and type `T`).
1. Look for local (non-quantified) assumptions for `[G] C T`.
2. Look for local quantified constraints whose conclusions match `C T`. If exactly one matches, select the constraint. Then, check whether any quantified constraints *unify* with `C T` (allowing any variables in `C T` to be bound). If any do, abort, complaining about potential incoherence. Otherwise, reduce `[W] C T` to the premise of the quantified constraint.
3. Same as (2), but using the global instance table.
**Proposal**:
Use specificity to disambiguate.
* Let `<=spec` denote a partial order on instance heads. `C T1 <=spec C T2` iff there exists a substitution `S` such that `S(T2) = T1` -- just as is used with overlapping instances today.
* Let metavariable `I` denote givens. These can be non-quantified, quantified (local), or global.
* Define `locality(I)` be a number that denotes how local `I` is. The locality of a non-quantified given is 1, of a quantified local given is 2, and of a global is 3.
* Define partial order `<=` on instances as follows:
1. If `I1 <=spec I2` and `I2 <=spec I1`, then `I1 <= I2` is `locality(I1) <= locality(I2)`.
2. If neither `I1 <=spec I2` nor `I2 <=spec I1`, then `I1 <= I2` is `locality(I1) <= locality(I2)`.
3. Otherwise, `I1 <= I2` if `I1 <=spec I2`.
Here is the proposed instance lookup procedure:
1. Collect all givens `I` (of all localities) that match a target. Call this set `Is`. If `Is` is empty, fail.
2. Let `I0` be the minimum element of `Is` with respect to `<=`. (Consider `Is` to be set-like, discarding duplicates.) If `I0` is not defined, fail.
3. Let `Is'` be the set `Is` excluding `I0`. Case on the locality of `I0`:
* `locality(I0) = 1`: Succeed with `I0` (skipping last check, below).
* `locality(I0) = 2`: Go on to next step if `Is'` contains only global instances. If `Is'` contains local instances, fail.
* `locality(I0) = 3`: Fail if any element in `Is'` is a local quantified instance. Go on to next step if, for every `I'` in `Is'`, either `I0` is *overlapping* or `I'` is *overlappable*.
4. Collect all givens (of all localities) that *unify* with a target, excluding those in `Is`. If `IncoherentInstances` is off and this set contains at least one instances not labeled **incoherent**, fail.
5. Succeed with `I0`.
**Discussion**:
This new algorithm is meant to replicate current behavior, except in the scenario where a global instance is more specific than a local one, in which the global instance should be selected. I have tried to capture current behavior w.r.t. incoherent and overlapping instances. In any case, if my algorithm deviates from current behavior w.r.t. incoherent or overlapping instances, this deviation is unintentional.
Another possible approach is to put local and global instances on even footing (that is, set both to have locality 2) but to allow users to explicitly label local instances as overlapping. I prefer the tiered approach above, but there's something simpler about local overlapping instances, in that it's one mechanism to think about.https://gitlab.haskell.org/ghc/ghc/-/issues/17873Lazy instantiation is incompatible with implicit parameters2020-07-15T09:06:16ZRichard Eisenbergrae@richarde.devLazy instantiation is incompatible with implicit parametersIn thinking about issues around #17173, I came up with this silliness:
```hs
getx :: (?x :: Bool -> Bool) => Bool -> Bool
getx = ?x
z3 = (let ?x = not in getx) False
```
GHC's current response is utter garbage:
```
Scratch.hs:52:23: ...In thinking about issues around #17173, I came up with this silliness:
```hs
getx :: (?x :: Bool -> Bool) => Bool -> Bool
getx = ?x
z3 = (let ?x = not in getx) False
```
GHC's current response is utter garbage:
```
Scratch.hs:52:23: error:
• Couldn't match type ‘?x::Bool -> Bool’ with ‘Bool’
Expected type: Bool -> Bool -> Bool
Actual type: (?x::Bool -> Bool) => Bool -> Bool
• In the expression: getx
In the expression: let ?x = not in getx
In the expression: (let ?x = not in getx) False
|
52 | z3 = (let ?x = not in getx) False
|
```
The "couldn't match type" bit is ill-kinded, and I have no idea why GHC is expecting `Bool -> Bool -> Bool` here. But the root cause, I believe, is lazy instantiation. Functions are instantiated lazily. So the `let ?x = not in getx` is instantiated lazily. The body of a `let` inherits its instantiation behavior from the outer context. So the `getx` is instantiated lazily. This means that GHC happily infers type `(?x :: Bool -> Bool) => Bool -> Bool` for `getx`. And then, with no incentive to instantiate, it infers `(let ?x = not in getx) :: (?x :: Bool -> Bool) => Bool -> Bool`. Now, when we apply such a thing to a term argument, GHC instantiates. But, lo!, there is no longer a `?x :: Bool -> Bool` constraint in scope, causing unhappiness.
If we instantiate eagerly, I claim this should all work just fine.
I believe this will be fixed alongside #17173, but given that #17173 is about general improvement rather than bug-fixing, I made this outright bug a separate ticket.https://gitlab.haskell.org/ghc/ghc/-/issues/17841"No skolem info" panic with PolyKinds2020-10-19T09:16:46ZJakob Brünker"No skolem info" panic with PolyKinds## Summary
Making a class with a kind-polymorphic parameter and a single method can lead to a GHC panic stating "No skolem info".
## Steps to reproduce
The following program
```haskell
{-# LANGUAGE PolyKinds #-}
data Proxy a = Proxy...## Summary
Making a class with a kind-polymorphic parameter and a single method can lead to a GHC panic stating "No skolem info".
## Steps to reproduce
The following program
```haskell
{-# LANGUAGE PolyKinds #-}
data Proxy a = Proxy
class Foo (t :: k) where foo :: Proxy (a :: t)
```
results in the error
```
Bug.hs:5:40: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.11.0.20200215:
No skolem info:
[k_a1q3[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1187:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2793:17 in ghc:TcErrors
```
On 8.6.5, it instead emits the error message
```
Bug.hs:5:45: error:
• Expected a type, but ‘t’ has kind ‘k’
• In the kind ‘t’
In the first argument of ‘Proxy’, namely ‘(a :: t)’
In the type signature: foo :: Proxy (a :: t)
|
5 | class Foo (t :: k) where foo :: Proxy (a :: t)
|
```
I thought at first it might be https://gitlab.haskell.org/ghc/ghc/issues/16245 but for the facts that that issue specifically mentions RankNTypes, and produces an error already on GHC 8.6, which this example doesn't.
## Expected behavior
It should probably emit the same error message it emitted in 8.6.
## Environment
* GHC versions used: 8.8.1, HEAD
* Does *not* happen on 8.6.5
Optional:
* Operating System: linux
* System Architecture: x86_648.10.2