GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2021-09-07T14:37:54Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/20318GHC complains about impredicativity in type synonym for a quantified constraint2021-09-07T14:37:54ZRichard Eisenbergrae@richarde.devGHC complains about impredicativity in type synonym for a quantified constraintIf I say
```hs
{-# LANGUAGE ConstraintKinds, QuantifiedConstraints #-}
module Bug where
type T b = (Ord b, forall a. Eq a)
```
then GHC HEAD says
```
Bug.hs:5:1: error:
• Illegal polymorphic type: forall a. Eq a
Perhaps yo...If I say
```hs
{-# LANGUAGE ConstraintKinds, QuantifiedConstraints #-}
module Bug where
type T b = (Ord b, forall a. Eq a)
```
then GHC HEAD says
```
Bug.hs:5:1: error:
• Illegal polymorphic type: forall a. Eq a
Perhaps you intended to use ImpredicativeTypes
• In the type synonym declaration for ‘T’
|
5 | type T b = (Ord b, forall a. Eq a)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Note that `T` defines a *constraint* synonym, not a type synonym. Accordingly, `QuantifiedConstraints` should be enough to accept this definition.
Inspired by https://mail.haskell.org/pipermail/haskell-cafe/2021-August/134388.htmlhttps://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/11581TypeError requires UndecidableInstances unnecessarily2021-08-03T22:02:50ZrwbartonTypeError requires UndecidableInstances unnecessarilyThe example from the `TypeError` documentation
```hs
type family ByteSize x where
ByteSize Word16 = 2
ByteSize Word8 = 1
ByteSize a = TypeError (Text "The type " :<>: ShowType a :<>:
...The example from the `TypeError` documentation
```hs
type family ByteSize x where
ByteSize Word16 = 2
ByteSize Word8 = 1
ByteSize a = TypeError (Text "The type " :<>: ShowType a :<>:
Text " is not exportable.")
```
requires `UndecidableInstances`:
```
BS.hs:11:5: error:
• The type family application ‘(TypeError ...)’
is no smaller than the instance head
(Use UndecidableInstances to permit this)
• In the equations for closed type family ‘ByteSize’
In the type family declaration for ‘ByteSize’
```
Obviously there's no real danger of undecidability here.
I tried changing the declaration of `TypeError` to
```hs
type family TypeError :: ErrorMessage -> b where
```
but it didn't help. Same error. Is that a bug?https://gitlab.haskell.org/ghc/ghc/-/issues/20146Unify wastes effort on casts2021-07-27T21:31:47ZSimon Peyton JonesUnify wastes effort on castsIn GHC.Core.Unify the main `unify_ty` function has signature
```
unify_ty :: UMEnv
-> Type -> Type -- Types to be unified and a co
-> CoercionN -- A coercion between their kinds
-- See Not...In GHC.Core.Unify the main `unify_ty` function has signature
```
unify_ty :: UMEnv
-> Type -> Type -- Types to be unified and a co
-> CoercionN -- A coercion between their kinds
-- See Note [Kind coercions in Unify]
-> UM ()
```
That `CoercionN`, called `kco` in code, is derived from the idea in `eqType` that we
are comparing types *ignoring casts*.
The point of this ticket is **we do not know a single example where carrying kco makes unification succeed, where
it would otherwise fail**.
The simpler alternative is to have
```
unify_ty :: UMEnv
-> Type -> Type
-> UM ()
```
and code like
```
unify_ty env (CastTy ty1' co1) (CastTy ty2 co2)
| isReflexiveCo (co1 `mkTransCo` sym co2)
= = unify_ty env ty1' ty2' (co1 `mkTransCo` kco `mkTransCo` mkSymCo co2)
unify_ty env (Cast {}) ty2 = surelyApart
unify_ty env ty1 (Cast {}) = surelyApart
```
You might think this would not work on something like
```
f :: t1 -> t2
x :: t1
f x ~ ((f |> co1) (x |> co2)) |> co3
where
co1 :: t1 -> t2 ~ t3 -> t4
co2 :: t1 ~ t3
co3 :: t4 ~ t2
```
But that's ruled out by invariant (EQ1) in `Note [Respecting definitional equality]` in GHC.Core.TyCo.Rep.
Similarly
```
(forall a. t1 |> co) ~ (forall a. t2) |> co2
```
is ruled out by (EQ4).Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/12652Type checker no longer accepting code using function composition and rank-n t...2021-07-11T13:33:45ZEdward Z. YangType checker no longer accepting code using function composition and rank-n typesThe following program (reduced from Cabal code that uses HasCallStack) typechecks in GHC 8.0, but not on HEAD:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ImplicitParams #-}
module Foo where
type T a = (?x :: Int) => a
type M a ...The following program (reduced from Cabal code that uses HasCallStack) typechecks in GHC 8.0, but not on HEAD:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ImplicitParams #-}
module Foo where
type T a = (?x :: Int) => a
type M a = T (IO a)
f :: T (T a -> a)
f x = x
g :: Int -> M ()
g = undefined
h :: Int -> M ()
-- h x = f (g x) -- works on HEAD
h = f . g -- fails on HEAD, works on GHC 8.0
```
It's possible that this is just fall out from the recent impredicativity changes but I just wanted to make sure that this was on purpose.Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/19974Non-terminating substitution with derived constraints2021-06-30T13:36:28Zsheafsam.derbyshire@gmail.comNon-terminating substitution with derived constraints@rae reports the following issue, introduced by the removal of flattening variables (8bb52d91).
```haskell
{-# LANGUAGE TypeFamilies, FunctionalDependencies, FlexibleInstances,
FlexibleContexts, ScopedTypeVariables #-}
mod...@rae reports the following issue, introduced by the removal of flattening variables (8bb52d91).
```haskell
{-# LANGUAGE TypeFamilies, FunctionalDependencies, FlexibleInstances,
FlexibleContexts, ScopedTypeVariables #-}
module Bug where
type family F a
class C a b | a -> b where
meth :: a -> b -> ()
g :: forall a b. (F b ~ F a) => a -> b -> ()
g x y = const () (meth True x, meth False y, [undefined :: F a, True])
```
```
* Reduction stack overflow; size = 201
When simplifying the following type: F a
Use -freduction-depth=0 to disable this check
(any upper bound you could choose might fail unpredictably with
minor updates to GHC, so disabling the check is recommended if
you're sure that type checking should terminate)
* In the expression: undefined :: F a
In the expression: [undefined :: F a, True]
In the second argument of `const', namely
`(meth True x, meth False y, [undefined :: F a, True])'
|
11 | g x y = const () (meth True x, meth False y, [undefined :: F a, True])
| ^^^^^^^^^^^^^^^^
```
The problem is that we end up with inerts:
```
[G] co {0} :: F b[sk:1] ~# F a[sk:1] (CEqCan)
[D] _ {0}:: a[sk:1] ~# b[sk:1] (CEqCan)
```
and work item
```
[D] _ {0}:: F a[sk:1] ~# Bool (CEqCan)
```
This causes a loop as the substitution associated to the inert set is not terminating, rewriting `F a` to `F b` (using the Derived) then back to `F a` (using the Given).
---------------------------------
Note that a similar situation can happen if we allow Wanteds to rewrite Wanteds (see test case `T3440`):
```haskell
type family Fam a :: Type
data GADT :: Type -> Type where
GADT :: a -> Fam a -> GADT (Fam a)
unwrap :: GADT (Fam a) -> (a, Fam a)
unwrap (GADT x y) = (x, y)
```
In that case we end up with inert set
```
[G] F b[sk:1] ~# F a[sk:1] (CEqCan)
[W] a[sk:1] ~# b[sk:1] (CEqCan)
```
which causes the same loop when trying to rewrite another wanted involving `a` or `b`.https://gitlab.haskell.org/ghc/ghc/-/issues/17368Implement homogeneous equality2021-06-16T15:54: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/dep-roles/dep-roles.pdf), the primitive equality type in GHC can be made homogeneous. T...As observed in [two](https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1076&context=compsci_pubs) [papers](https://richarde.dev/papers/2019/dep-roles/dep-roles.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 type-checker 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/dependent-haskell/phase2, which has much discussion.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/19929Using equality constraint in datatype kind signature leads to various strange...2021-06-14T04:47:03ZJakob BrünkerUsing equality constraint in datatype kind signature leads to various strange behaviorsThe following file
```haskell
{-# LANGUAGE DataKinds , TypeFamilies #-}
module Weird where
import Data.Kind
type Weird :: forall a -> (a ~ Char) => Type
data Weird a = MkWeird a
deriving Show
```
allows this GHCi session:
...The following file
```haskell
{-# LANGUAGE DataKinds , TypeFamilies #-}
module Weird where
import Data.Kind
type Weird :: forall a -> (a ~ Char) => Type
data Weird a = MkWeird a
deriving Show
```
allows this GHCi session:
```haskell
ghci> :t MkWeird
-- This looks like a kind error, and is impossible to write
MkWeird :: forall a {ev :: a ~ Char}. a -> Weird a
ghci> MkWeird "foo"
-- this is fine - but shouldn't be! The argument to MkWeird must be a Char, not String
MkWeird "foo"
ghci> :t MkWeird "foo"
-- We can ask for the type
MkWeird "foo" :: Weird String
ghci> :t MkWeird "foo" :: Weird String
-- but checking that same type results in a kind error
-- (shouldn't this be a type error instead?)
<interactive>:1:18: error:
* Couldn't match kind `[Char]' with `Char'
[...]
ghci> import Data.Dynamic
ghci> Data.Dynamic.toDyn (MkWeird 'c' :: Weird Char)
-- what is <>?
<interactive>:50:1: error:
* No instance for (Typeable <>) arising from a use of `toDyn'
[...]
ghci> :i Show
-- The derived Show instance would be impossible to write manually
[...]
instance forall a (ev :: a ~ Char). Show a => Show (Weird a)
[...]
```
## Environment
* GHC version used: 9.3.20210529
Optional:
* Operating System: Arch on WSL2 on Windows 10
* System Architecture: x86_64https://gitlab.haskell.org/ghc/ghc/-/issues/19855Wired-in names in hs-boot files are not fully checked2021-05-20T11:45:02ZSylvain HenryWired-in names in hs-boot files are not fully checked#19638 was due to a declaration in a hs-boot file of ghc-bignum not matching the declaration in the corresponding hs file.
In https://gitlab.haskell.org/ghc/ghc/-/issues/19638#note_352989 @mpickering noticed that it is because wired-in ...#19638 was due to a declaration in a hs-boot file of ghc-bignum not matching the declaration in the corresponding hs file.
In https://gitlab.haskell.org/ghc/ghc/-/issues/19638#note_352989 @mpickering noticed that it is because wired-in names bypass some checks (see https://gitlab.haskell.org/ghc/ghc/-/blob/fc9546caf3e16db070bfc7bb5523c38595233e26/compiler/GHC/Tc/Module.hs#L870)
We should be more selective about the wired-in names that need this special treatment (which has been added in 5ad61e1470db6dbc8279569c5ad1cc093f753ac0).
Moreover the comment there says that it's used in particular for `GHC.Err.error` because it's a rather gross hack, but `libraries/base/GHC/Err.lhs-boot` doesn't exist since 404327a9d9ce38804c5e407eaf2a4167e9a3c906 and `error` isn't wired-in since a7b751db766bd456ace4f76a861e5e8b927d8f17.https://gitlab.haskell.org/ghc/ghc/-/issues/19726Unexpected type-checking behavior with let and DataKinds2021-05-10T12:28:34ZbenjaminUnexpected type-checking behavior with let and DataKinds## Motivation
When playing around with the code for known-length vectors from #19722, I noticed following behavior in the type-checker when trying to implement a function to get the last element of a vector.
```
last :: Vec (Succ n) a ...## Motivation
When playing around with the code for known-length vectors from #19722, I noticed following behavior in the type-checker when trying to implement a function to get the last element of a vector.
```
last :: Vec (Succ n) a -> a
last (x :> Nil) = x
last (_ :> xs) = case xs of x' :> xs' -> last xs
--last (_ :> xs) = let (x' :> xs') = xs in last xs
--last (_ :> xs) = let (x' :> xs') = xs in last (x' :> xs')
```
The main issue here is that we can't just write `last (_ :> xs) = last xs`, because then GHC can't verify that the type of `xs` is really `Vec (Succ n) a`.
So the workaround is to let GHC know that `xs` is really non-empty in this second case.
The first version of the case `_ :> xs` using a case-expression compiles fine, but the two version implemented using let-expressions don't type-check.
I lack an in-depth understanding of the type-checker or even the DataKinds extension, but I think the 3 versions are semantically identical.
## Proposal
Make all 3 versions type-check.https://gitlab.haskell.org/ghc/ghc/-/issues/19787Weird behaviour with `tcIfaceExpr`2021-05-03T17:41:43ZJosh MeredithWeird behaviour with `tcIfaceExpr`When recovering the Core AST of a class method in a plugin through multiple methods, the type-check loaded (deserialised) AST appears to be using the wrong expression for certain methods. This occurs both using ASTs recovered from the pr...When recovering the Core AST of a class method in a plugin through multiple methods, the type-check loaded (deserialised) AST appears to be using the wrong expression for certain methods. This occurs both using ASTs recovered from the pre-existing unfoldings, as well as when using the `toIfaceBind` and `tcIfaceExpr` functions from GHC to (de)serialise the bindings via an extensible interface field.
As an example, using the following type class and instances:
```haskell
class TwoClass a where
twoA :: a -> Integer
twoB :: a -> Bool
instance TwoClass Integer where
twoA = id
twoB = (>1)
instance TwoClass Bool where
twoA True = 1
twoA False = 0
twoB = not
```
_Before_ serialisation, from the `CgGuts.cgBinds`, we have class methods that look like:
```
twoA :: forall a. TwoClass a => a -> Integer
[GblId[ClassOp],
Arity=1,
Caf=NoCafRefs,
Str=<SP(SL,A)>,
RULES: Built in rule for twoA: "Class op twoA"]
twoA
= \ (@a) (v_B1 :: TwoClass a) ->
case v_B1 of v_B1 { C:TwoClass v_B2 v_B3 -> v_B2 },
twoB :: forall a. TwoClass a => a -> Bool
[GblId[ClassOp],
Arity=1,
Caf=NoCafRefs,
Str=<SP(A,SL)>,
RULES: Built in rule for twoB: "Class op twoB"]
twoB
= \ (@a) (v_B1 :: TwoClass a) ->
case v_B1 of v_B1 { C:TwoClass v_B2 v_B3 -> v_B3 }
```
Each of the class methods is deconstructed as a data constructor and obviously uses the correct field of that constructor as the method. However, after round-tripping this through (de)serialisation, we're have:
```
twoA :: forall a. TwoClass a => a -> Integer
[LclId]
twoA
= \ (@a) (v :: TwoClass a) -> case v of v { C:TwoClass v v -> v },
twoB :: forall a. TwoClass a => a -> Bool
[LclId]
twoB
= \ (@a) (v :: TwoClass a) -> case v of v { C:TwoClass v v -> v }
```
Now, the reuse of the variable name `v` shouldn't be a problem on it's own - since these local variables are serialised as `FastStrings`, which have `Unique`s - but we find in the plugin that for `twoA`, it's the _wrong_ `Unique`, incorrectly giving `twoA` an expression of type `a -> Bool`.
We're using GHC 8.10.4 for the Plutus plugin, but I've tested and found what seems to be the same behaviour in an up-to-date version of master. I expect that there must be another explanation here, since unfoldings are used by GHC for inlining, and I don't believe those would go unnoticed if broken.https://gitlab.haskell.org/ghc/ghc/-/issues/19652GHC's failure to rewrite in coercions & kinds leads to spurious occurs-check ...2021-04-08T08:48:53ZRichard Eisenbergrae@richarde.devGHC's failure to rewrite in coercions & kinds leads to spurious occurs-check failureConsider this mess:
```hs
{-# LANGUAGE ExplicitForAll, PolyKinds, DataKinds, TypeFamilies,
StandaloneKindSignatures, AllowAmbiguousTypes, GADTs,
TypeOperators #-}
module Bug where
import Data.Kind ( Type )
im...Consider this mess:
```hs
{-# LANGUAGE ExplicitForAll, PolyKinds, DataKinds, TypeFamilies,
StandaloneKindSignatures, AllowAmbiguousTypes, GADTs,
TypeOperators #-}
module Bug where
import Data.Kind ( Type )
import Data.Type.Equality ( type (~~) )
import Data.Proxy ( Proxy )
type Const :: () -> k1 -> k2 -> k1
type family Const u x y where
Const '() x y = x
type Equals :: k1 -> k2 -> Type
type family Equals a b where
Equals a a = Char
Equals a b = Bool
type IsUnit :: () -> Type
data IsUnit u where
ItIs :: IsUnit '()
f :: forall (u :: ()) (a :: Type) (b :: Const u Type a). (a ~~ b)
=> IsUnit u -> a -> Proxy b -> Equals a b
f ItIs _ _ = 'x'
g = f ItIs
```
GHC fails (in the RHS of `g`) with an occurs-check, but it should succeed.
The problem is that we end up with
```
[W] (alpha :: Type) ~# (beta :: Const upsilon Type alpha)
```
where we have already unified `upsilon := '()`.
But GHC refuses to rewrite in kinds, so the `Const` never reduces, and we reject the program. Note that a solution exists, with `alpha := Any @Type` and `beta := Any @Type |> sym (AxConst Type (Any @Type))`.
Proposed solution:
The wanted above actually gets simplified to become
```
[W] co :: Const '() Type alpha ~# Type
[W] w2 :: (alpha :: Type) ~# ((beta |> co) :: Type)
```
The `co` is easily solved. Then, when we get to `w2`, we are in Wrinkle (3) of Note [Equalities with incompatible kinds]. Happily, we should be able to detect that `alpha` is free in `co` and reorient, giving
```
[W] w3 :: (beta :: Const '() Type alpha) ~# (alpha |> sym co :: Const '() Type alpha)
```
which can be solved by unifying `beta := alpha |> sym co`. `alpha` will then remain unconstrained and will be zonked to `Any`.
The key new part is looking at the coercion when deciding whether to reorient.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/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/16422Inconsistent results with inaccessible code due to (~) vs. (~~)2021-03-19T14:20:05ZRyan ScottInconsistent results with inaccessible code due to (~) vs. (~~)The following code typechecks:
```haskell
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Type.Equality
data T = (Int ~ Char) => MkT { fld :: Int }
```
```
$ /opt/ghc/8.6.3/bin/ghci Bug.hs
GHCi, vers...The following code typechecks:
```haskell
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Type.Equality
data T = (Int ~ Char) => MkT { fld :: Int }
```
```
$ /opt/ghc/8.6.3/bin/ghci Bug.hs
GHCi, version 8.6.3: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:7:32: warning: [-Winaccessible-code]
• Couldn't match type ‘Int’ with ‘Char’
Inaccessible code in
a pattern with constructor: MkT :: (Int ~ Char) => Int -> T,
in an equation for ‘fld’
• In the pattern: MkT {fld = fld}
In an equation for ‘fld’: fld MkT {fld = fld} = fld
|
7 | data T = (Int ~ Char) => MkT { fld :: Int }
| ^^^
```
It produces a warning, of course, since there's no way to ever actually invoke `fld`.
The interesting part of this is that if you replace `~` with `~~` in this program, then GHC will switch from accepting to rejecting it:
```haskell
data T = (Int ~~ Char) => MkT { fld :: Int }
```
```
$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:7:10: error:
• Couldn't match expected type ‘Char’ with actual type ‘Int’
• In the ambiguity check for ‘MkT’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the definition of data constructor ‘MkT’
In the data type declaration for ‘T’
|
7 | data T = (Int ~~ Char) => MkT { fld :: Int }
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This feels strangely inconsistent.
-----
A similar phenomenon occurs in function definitions. This function is accepted (with no warnings):
```haskell
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Type.Equality
f :: (Int ~ Char) => () -> ()
f () = ()
```
But it is no longer accepted when `~` is swapped out with `~~`:
```haskell
f :: (Int ~~ Char) => () -> ()
f () = ()
```
```
$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:7:6: error:
• Couldn't match expected type ‘Char’ with actual type ‘Int’
• In the ambiguity check for ‘f’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: f :: (Int ~~ Char) => () -> ()
|
7 | f :: (Int ~~ Char) => () -> ()
| ^^^^^^^^^^^^^^^^^^^^^^^^^
```https://gitlab.haskell.org/ghc/ghc/-/issues/17223Slow Typechecking (Followup of #14987)2021-03-12T23:10:14ZVictor Cacciari MiraldoSlow Typechecking (Followup of #14987)## Summary
Type Checking consumes an exponential amount of memory and is consequently very slow
in the presence of complicated pattern matching. This is a followup of #14987
The attached files have been generated with Template Haskell...## Summary
Type Checking consumes an exponential amount of memory and is consequently very slow
in the presence of complicated pattern matching. This is a followup of #14987
The attached files have been generated with Template Haskell and are essentially
a self-contained version of a `stack build --ghc-options="-ddump-splices -ddump-to-file"`
of [this repository](https://github.com/VictorCMiraldo/hdiff).
## Steps to reproduce
Compile the attached files. Might be a good idea to `ulimit -m`
the shell before calling the compiler to prevent the machine from freezing.
[Go-hdiff-900744.hs](/uploads/7f9597aa8b49c9d360e382d8309385ce/Go-hdiff-900744.hs)
[Python-hdiff-e009013.hs](/uploads/42d08a992ed30ab15f905f8a0f75ca32/Python-hdiff-e009013.hs)
### Structure of Attached Files
The structure of the attached files is simple, but very long and mechanical (hence why we are
using TH!). It consists of a generic instance for mutually recursive types using the `generics-mrsop` library.
For example,
```haskell
data A = A0 Int | A1 B
data B = B0 Char | B1 A
-- Now, call the TH to generate the monstrous code
deriveFamily ''Singl [t| A |]
```
would yield something in the lines of
```haskell
type FamA = [ A , B ]
type CodesA = [ [ [ Int ] , [I (S Z)] ]
, [ [ Char ], [I Z] ] ]
instance Family Singl FamA CodesA where
sfrom SZ (A0 c) = Rep (Here (c :* Nil))
sfrom SZ (A1 b) = Rep (There (Here (b :* Nil))
sfrom (SS SZ) (B0 c) = Rep (Here (c :* Nil))
sfrom (SS SZ) (B1 a) = Rep (Here (There (a :* Nil))
sto ... -- inverse of sfrom
```
The attached files are the versions we get from attempting to use `language-go` or `language-python` with
`generics-mrsop`.
## Environment
* GHC version used: 8.4.2, 8.6.5https://gitlab.haskell.org/ghc/ghc/-/issues/344arrow notation: incorrect scope of existential dictionaries2021-03-12T11:26:40Znobodyarrow notation: incorrect scope of existential dictionaries```
ghc-6.4: panic! (the `impossible' happened, GHC version
6.4):
cgPanic
deref{v a1yz}
static binds for:
local binds for:
SRT labelghc-6.4: panic! (the `impossible'
happened, GHC version 6.4):
initC: srt
...```
ghc-6.4: panic! (the `impossible' happened, GHC version
6.4):
cgPanic
deref{v a1yz}
static binds for:
local binds for:
SRT labelghc-6.4: panic! (the `impossible'
happened, GHC version 6.4):
initC: srt
Please report it as a compiler bug to
glasgow-haskell-bugs@haskell.org,
or http://sourceforge.net/projects/ghc/.
I've attached a test driver that can reproduce the problem.
-- Esa Pulkkinen <esa.pulkkinen@kotiposti.net>
```8.0.1Ross Patersonr.paterson@city.ac.ukRoss Patersonr.paterson@city.ac.ukhttps://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/13655Spurious untouchable type variable in connection with rank-2 type and constra...2021-02-15T03:51:51ZWolfgang JeltschSpurious untouchable type variable in connection with rank-2 type and constraint familyThe following code cannot be compiled:
```hs
{-# LANGUAGE ConstraintKinds, Rank2Types, TypeFamilies #-}
import GHC.Exts (Constraint)
type family F a b :: Constraint
data T b c = T
f :: (forall b . F a b => T b c) -> a
f _ = undefine...The following code cannot be compiled:
```hs
{-# LANGUAGE ConstraintKinds, Rank2Types, TypeFamilies #-}
import GHC.Exts (Constraint)
type family F a b :: Constraint
data T b c = T
f :: (forall b . F a b => T b c) -> a
f _ = undefined
```
GHC outputs the following error message:
```
Untouchable.hs:9:6: error:
• Couldn't match type ‘c0’ with ‘c’
‘c0’ is untouchable
inside the constraints: F a b
bound by the type signature for:
f :: F a b => T b c0
at Untouchable.hs:9:6-37
‘c’ is a rigid type variable bound by
the type signature for:
f :: forall a c. (forall b. F a b => T b c) -> a
at Untouchable.hs:9:6
Expected type: T b c0
Actual type: T b c
• In the ambiguity check for ‘f’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature:
f :: (forall b. F a b => T b c) -> a
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1-rc2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Spurious untouchable type variable in connection with rank-2 type and constraint family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1-rc2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code cannot be compiled:\r\n{{{#!hs\r\n{-# LANGUAGE ConstraintKinds, Rank2Types, TypeFamilies #-}\r\n\r\nimport GHC.Exts (Constraint)\r\n\r\ntype family F a b :: Constraint\r\n\r\ndata T b c = T\r\n\r\nf :: (forall b . F a b => T b c) -> a\r\nf _ = undefined\r\n}}}\r\nGHC outputs the following error message:\r\n{{{\r\nUntouchable.hs:9:6: error:\r\n • Couldn't match type ‘c0’ with ‘c’\r\n ‘c0’ is untouchable\r\n inside the constraints: F a b\r\n bound by the type signature for:\r\n f :: F a b => T b c0\r\n at Untouchable.hs:9:6-37\r\n ‘c’ is a rigid type variable bound by\r\n the type signature for:\r\n f :: forall a c. (forall b. F a b => T b c) -> a\r\n at Untouchable.hs:9:6\r\n Expected type: T b c0\r\n Actual type: T b c\r\n • In the ambiguity check for ‘f’\r\n To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n In the type signature:\r\n f :: (forall b. F a b => T b c) -> a\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/16947Refactor Ct and friends2021-01-22T23:50:33ZRichard Eisenbergrae@richarde.devRefactor Ct and friendsRight now, the `Ct` type contains many constructors. This ticket tracks breaking up this type into smaller ones. Candidates:
* All constraints are born as non-canonical. So the bag of constraints in the `TcM` monad are all non-canonical...Right now, the `Ct` type contains many constructors. This ticket tracks breaking up this type into smaller ones. Candidates:
* All constraints are born as non-canonical. So the bag of constraints in the `TcM` monad are all non-canonical. This should be its own type.
* Equality constraints are dealt with separately from others. (See details on the description of the inert set.) These should be their own types, too.
* A work list has both canonical and non-canonical constraints. But this might be the only place we need the full sum.9.2.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/13361Better type synonym merging/subtyping for Backpack2021-01-07T15:23:37ZEdward Z. YangBetter type synonym merging/subtyping for BackpackHere are two signatures which don't merge today in Backpack:
```
signature A where
data T
data U = Mk T
signature A where
data S
data U = Mk S
```
On the one hand, this is not too surprising, because you never said that...Here are two signatures which don't merge today in Backpack:
```
signature A where
data T
data U = Mk T
signature A where
data S
data U = Mk S
```
On the one hand, this is not too surprising, because you never said that T and S were the same, so why should I decide that the declarations of U are compatible? OK, but suppose I were to add the missing type synonym: which direction should I put it? What you will find is that, under Backpack's current subtyping rules, \*neither\* orientation is a subtype of the other:
```
signature A where
data T
type S = T
data U = Mk T
signature A where
type T = S
data S
data U = Mk S
```
The first signature is a supertype of a module that says `data T = MkCommon`, but NOT of a module that says `data S = MkCommon`, since type synonym declarations and data declarations are not compatible.
This doesn't smell very good. Indeed, ML's semantic signatures do not have this problem, because when I write these signatures, I actually get a semantic signature of the form `exists c. { type T = c, type S = c, ... }`; i.e., neither declaration is privileged.
On the other hand, our behavior is inline with MixML, which does not have these as mutual subtypes. So it's not clear the complexity of changing our internal language justifies the marginal benefit that is to be gotten here. Not planning on fixing this unless someone shouts.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | low |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Better type synonym merging/subtyping for Backpack","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["backpack"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Here are two signatures which don't merge today in Backpack:\r\n\r\n{{{\r\nsignature A where\r\n data T\r\n data U = Mk T\r\nsignature A where\r\n data S\r\n data U = Mk S\r\n}}}\r\n\r\nOn the one hand, this is not too surprising, because you never said that T and S were the same, so why should I decide that the declarations of U are compatible? OK, but suppose I were to add the missing type synonym: which direction should I put it? What you will find is that, under Backpack's current subtyping rules, *neither* orientation is a subtype of the other:\r\n\r\n{{{\r\nsignature A where\r\n data T\r\n type S = T\r\n data U = Mk T\r\nsignature A where\r\n type T = S\r\n data S\r\n data U = Mk S\r\n}}}\r\n\r\nThe first signature is a supertype of a module that says `data T = MkCommon`, but NOT of a module that says `data S = MkCommon`, since type synonym declarations and data declarations are not compatible.\r\n\r\nThis doesn't smell very good. Indeed, ML's semantic signatures do not have this problem, because when I write these signatures, I actually get a semantic signature of the form `exists c. { type T = c, type S = c, ... }`; i.e., neither declaration is privileged.\r\n\r\nOn the other hand, our behavior is inline with MixML, which does not have these as mutual subtypes. So it's not clear the complexity of changing our internal language justifies the marginal benefit that is to be gotten here. Not planning on fixing this unless someone shouts.","type_of_failure":"OtherFailure","blocking":[]} -->