GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2021-01-18T17:11:59Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/19197‘:kind () :: '()’ doesn't give any output2021-01-18T17:11:59ZIcelandjack‘:kind () :: '()’ doesn't give any output```
$ ./ghc/_build/stage1/bin/ghc -ignore-dot-ghci --interactive
GHCi, version 9.1.0.20201202: https://www.haskell.org/ghc/ :? for help
ghci> :set -XKindSignatures -XDataKinds
ghci> :k () :: '()
ghci>
ghci> :set -XPartialTypeSignatures ...```
$ ./ghc/_build/stage1/bin/ghc -ignore-dot-ghci --interactive
GHCi, version 9.1.0.20201202: https://www.haskell.org/ghc/ :? for help
ghci> :set -XKindSignatures -XDataKinds
ghci> :k () :: '()
ghci>
ghci> :set -XPartialTypeSignatures -Wno-partial-type-signatures
ghci> :k (_, _) :: '(_, _)
ghci>
ghci> import Data.Functor.Identity
ghci> :k Identity _ :: 'Identity _
ghci>
```
It should give an errorhttps://gitlab.haskell.org/ghc/ghc/-/issues/19315GHC 9.0 regression: plots-0.1.1.2 fails to build due to ambiguous type variable2021-02-10T21:11:55ZRyan ScottGHC 9.0 regression: plots-0.1.1.2 fails to build due to ambiguous type variable_Originally observed in a `head.hackage` CI build [here](https://gitlab.haskell.org/ghc/head.hackage/-/jobs/568397#L5617)_.
The `plots-0.1.1.2` library fails to compile using commit 0789f7a18a78920f50647e2b4aa8082a14ca9e90 of the `ghc-9..._Originally observed in a `head.hackage` CI build [here](https://gitlab.haskell.org/ghc/head.hackage/-/jobs/568397#L5617)_.
The `plots-0.1.1.2` library fails to compile using commit 0789f7a18a78920f50647e2b4aa8082a14ca9e90 of the `ghc-9.0` branch. Here is a self-contained example with no external dependencies:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Control.Monad.Reader
import Data.Functor.Const
import Data.Functor.Identity
import Data.Monoid (Any(..))
import Data.Typeable
type TypeableFloat n = (Typeable n, RealFloat n)
type Lens' s a = Lens s s a a
type Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t
type LensLike' f s a = LensLike f s s a a
type LensLike f s t a b = (a -> f b) -> s -> f t
type Getting r s a = (a -> Const r a) -> s -> Const r s
type ASetter s t a b = (a -> Identity b) -> s -> Identity t
data V2 a = V2 !a !a
flipX_Y :: Num n => V2 n -> V2 n
flipX_Y (V2 x y) = V2 (-y) (-x)
class R1 t where
_x :: Lens' (t a) a
class R1 t => R2 t where
_y :: Lens' (t a) a
instance R1 V2 where
_x f (V2 a b) = (`V2` b) <$> f a
instance R2 V2 where
_y f (V2 a b) = V2 a <$> f b
infixl 8 #
(#) :: a -> (a -> b) -> b
(#) = flip ($)
infixr 4 %~
(%~) :: ASetter s t a b -> (a -> b) -> s -> t
(%~) = over
(^.) :: s -> Getting a s a -> a
s ^. l = getConst (l Const s)
over :: ASetter s t a b -> (a -> b) -> s -> t
over l f = runIdentity . l (Identity . f)
view :: MonadReader s m => Getting a s a -> m a
view l = asks (getConst . l Const)
lens :: (s -> a) -> (s -> b -> t) -> Lens s t a b
lens sa sbt afb s = sbt s <$> afb (sa s)
type family V a :: * -> *
type family N a :: *
type Vn a = V a (N a)
data Style (v :: * -> *) n = Style
class HasStyle a where
applyStyle :: Style (V a) (N a) -> a -> a
type TextFunction b v n = TextAlignment n -> String -> QDiagram b v n Any
data TickLabels b (v :: * -> *) n = TickLabels
{ tlFun :: [n] -> (n,n) -> [(n, String)]
, tlTextFun :: TextFunction b v n
, tlStyle :: Style v n
, tlGap :: n
}
type instance V (TickLabels b v n) = v
type instance N (TickLabels b v n) = n
class HasTickLabels f a b | a -> b where
tickLabel :: LensLike' f a (TickLabels b (V a) (N a))
tickLabelTextFunction :: Functor f => LensLike' f a (TextFunction b (V a) (N a))
tickLabelTextFunction = tickLabel . lens tlTextFun (\tl f -> tl {tlTextFun = f})
tickLabelFunction :: Functor f => LensLike' f a ([N a] -> (N a, N a) -> [(N a, String)])
tickLabelFunction = tickLabel . lens tlFun (\tl f -> tl {tlFun = f})
tickLabelStyle :: Functor f => LensLike' f a (Style (V a) (N a))
tickLabelStyle = tickLabel . lens tlStyle (\tl sty -> tl {tlStyle = sty})
tickLabelGap :: Functor f => LensLike' f a (N a)
tickLabelGap = tickLabel . lens tlGap (\tl n -> tl {tlGap = n})
instance HasTickLabels f (TickLabels b v n) b where
tickLabel = id
data ColourBar b n = ColourBar
{ cbTickLabels :: TickLabels b V2 n
, cbTicks :: MajorTicks V2 n
, cbWidth :: n
}
type instance V (ColourBar b n) = V2
type instance N (ColourBar b n) = n
data MajorTicks (v :: * -> *) n = MajorTicks
{ matFunction :: (n,n) -> [n]
}
type instance V (MajorTicks v n) = v
type instance N (MajorTicks v n) = n
class HasMajorTicks f a where
majorTicks :: LensLike' f a (MajorTicks (V a) (N a))
majorTicksFunction :: Functor f => LensLike' f a ((N a, N a) -> [N a])
majorTicksFunction = majorTicks . lens matFunction (\mat a -> mat {matFunction = a})
instance HasMajorTicks f (MajorTicks v n) where
majorTicks = id
data Path (v :: * -> *) n = Path
data (:-:) u v = (u -> v) :-: (v -> u)
infixr 7 :-:
instance Semigroup (a :-: a) where
(f :-: f') <> (g :-: g') = f . g :-: g' . f'
instance Monoid (v :-: v) where
mempty = id :-: id
data Transformation v n = Transformation (v n :-: v n) (v n :-: v n) (v n)
class Transformable t where
transform :: Transformation (V t) (N t) -> t -> t
translation :: v n -> Transformation v n
translation = Transformation mempty mempty
translate :: (Transformable t) => Vn t -> t -> t
translate = transform . translation
class Transformable t => Renderable t b where
orient :: HasOrientation o => o -> a -> a -> a
orient o h v =
case view orientation o of
Horizontal -> h
Vertical -> v
data Orientation = Horizontal | Vertical
class HasOrientation a where
orientation :: Lens' a Orientation
instance HasPlacement (ColourBar b n) where
placement = undefined
instance HasOrientation (ColourBar b n) where
orientation = undefined
instance Functor f => HasMajorTicks f (ColourBar b n) where
majorTicks = lens cbTicks (\c a -> c {cbTicks = a})
data ColourMap = ColourMap
data QDiagram b (v :: * -> *) n m = QD
instance Semigroup m -- (Metric v, OrderedField n, Semigroup m)
=> HasStyle (QDiagram b v n m) where
applyStyle = undefined
instance Semigroup m -- (Metric v, OrderedField n, Semigroup m)
=> Monoid (QDiagram b v n m) where
mempty = undefined
instance Semigroup m -- (Metric v, OrderedField n, Semigroup m)
=> Semigroup (QDiagram b v n m) where
(<>) = undefined
instance Semigroup m -- (OrderedField n, Metric v, Semigroup m)
=> Transformable (QDiagram b v n m) where
transform = undefined
type instance V (QDiagram b v n m) = v
type instance N (QDiagram b v n m) = n
data TextAlignment n = BaselineText | BoxAlignedText n n
data Placement = Placement
{ pAt :: V2 Rational
}
class HasPlacement a where
placement :: Lens' a Placement
placementAt :: Lens' a (V2 Rational)
placementAt = placement . lens pAt (\p a -> p {pAt = a})
renderColourBar
:: forall n b. (TypeableFloat n, Renderable (Path V2 n) b)
=> ColourBar b n
-> ColourMap
-> (n,n)
-> n
-> QDiagram b V2 n Any
renderColourBar cb@ColourBar {..} _cm bnds@(lb,ub) l
= tLbs
where
o, xy :: a -> a -> a
o = orient cb
xy a b = if let V2 x y = cb^.placementAt in x > y
then a else b
w = cbWidth
f x = (x - (ub + lb)/2) / (ub - lb) * l
inRange x = x >= lb && x <= ub
tickXs = view majorTicksFunction cbTicks bnds
tickXs' :: [n]
tickXs' = filter inRange tickXs
tickLabelXs :: [(n, String)]
tickLabelXs = view tickLabelFunction cbTickLabels tickXs' bnds
tLbs :: QDiagram b V2 n Any
tLbs = foldMap drawTickLabel tickLabelXs
drawTickLabel :: (n, String) -> QDiagram b (V (TickLabels b V2 n)) (N (TickLabels b V2 n)) Any
drawTickLabel (x,label) =
view tickLabelTextFunction cbTickLabels tAlign label
# translate v
# applyStyle (cbTickLabels ^. tickLabelStyle)
where v = V2 (f x) (- w/2 - view tickLabelGap cbTickLabels)
# xy id (_y %~ negate)
# o id ((_y %~ negate) . flipX_Y)
tAlign = o (xy (BoxAlignedText 0.5 1) (BoxAlignedText 0.5 0))
(xy (BoxAlignedText 0 0.5) (BoxAlignedText 1 0.5))
```
This compiles with GHC 8.10.3 and earlier, but fails to compile with `ghc-9.0`:
```
$ ~/Software/ghc-9.0.0.20210130/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:229:22: error:
• Could not deduce (HasTickLabels
(Const ([n] -> (n, n) -> [(n, String)])) (TickLabels b V2 n) b0)
arising from a use of ‘tickLabelFunction’
from the context: (TypeableFloat n, Renderable (Path V2 n) b)
bound by the type signature for:
renderColourBar :: forall n b.
(TypeableFloat n, Renderable (Path V2 n) b) =>
ColourBar b n
-> ColourMap -> (n, n) -> n -> QDiagram b V2 n Any
at Bug.hs:(204,1)-(210,24)
The type variable ‘b0’ is ambiguous
Relevant bindings include
tickLabelXs :: [(n, String)] (bound at Bug.hs:229:3)
tickXs' :: [n] (bound at Bug.hs:226:3)
inRange :: n -> Bool (bound at Bug.hs:222:3)
tickXs :: [n] (bound at Bug.hs:224:3)
l :: n (bound at Bug.hs:211:52)
ub :: n (bound at Bug.hs:211:48)
cbTickLabels :: TickLabels b V2 n (bound at Bug.hs:211:31)
(Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)
These potential instance exist:
instance HasTickLabels f (TickLabels b v n) b
-- Defined at Bug.hs:100:10
• In the first argument of ‘view’, namely ‘tickLabelFunction’
In the expression: view tickLabelFunction cbTickLabels tickXs' bnds
In an equation for ‘tickLabelXs’:
tickLabelXs = view tickLabelFunction cbTickLabels tickXs' bnds
|
229 | tickLabelXs = view tickLabelFunction cbTickLabels tickXs' bnds
| ^^^^^^^^^^^^^^^^^
```
Moreover, this compiles with GHC 9.0.1-rc1. This regression was introduced at some point between the following commits:
* 9183f5a537df159e37c26d9d385cf497bcfaae30 (`gitlab-ci: Don't run LLVM tests on Debian 9`). This commit has an artifact associated with it, and I can confirm that the bug is not present here.
* 0789f7a18a78920f50647e2b4aa8082a14ca9e90 (`Hadrian: show default ghc-bignum backend (fix #18912)`)9.0.2https://gitlab.haskell.org/ghc/ghc/-/issues/19364oversized source range in type error message2021-03-04T10:42:13Zjwaldmannoversized source range in type error messageFor this code
```
type Foo = Bool
type Bar = String
data Pair a b = Pair a b
baz :: Pair Foo Bar
baz = Pair "yes" "no"
```
ghc says
```
B.hs:7:7-21: error:
• Couldn't match type ‘[Char]’ with ‘Bool’
Expected type: Pair Foo Ba...For this code
```
type Foo = Bool
type Bar = String
data Pair a b = Pair a b
baz :: Pair Foo Bar
baz = Pair "yes" "no"
```
ghc says
```
B.hs:7:7-21: error:
• Couldn't match type ‘[Char]’ with ‘Bool’
Expected type: Pair Foo Bar
Actual type: Pair [Char] [Char]
• In the expression: Pair "yes" "no"
In an equation for ‘baz’: baz = Pair "yes" "no"
|
7 | baz = Pair "yes" "no"
| ^^^^^^^^^^^^^^^
```
So, which argument is wrong?
In fact, how many are?
```
baz :: Pair Foo Bar
baz = Pair "yes" ()
B.hs:7:7-19: error:
• Couldn't match type ‘[Char]’ with ‘Bool’
Expected type: Pair Foo Bar
Actual type: Pair [Char] ()
• In the expression: Pair "yes" ()
In an equation for ‘baz’: baz = Pair "yes" ()
|
7 | baz = Pair "yes" ()
| ^^^^^^^^^^^^^
```
The following case works better (it shows that the first argument is the problem). What's the difference?
```
foo :: (Foo,Bar)
foo = ("yes", "no")
B.hs:11:8-12: error:
• Couldn't match type ‘[Char]’ with ‘Bool’
Expected type: Foo
Actual type: [Char]
• In the expression: "yes"
In the expression: ("yes", "no")
In an equation for ‘foo’: foo = ("yes", "no")
|
11 | foo = ("yes", "no")
| ^^^^^
```https://gitlab.haskell.org/ghc/ghc/-/issues/19419GHC 9.0 unable to deduce that instance signature is at least as general as cl...2021-02-25T03:14:03Zsheafsam.derbyshire@gmail.comGHC 9.0 unable to deduce that instance signature is at least as general as class signatureThe following program compiles OK on GHC 8.10 but not on GHC 9.0:
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module B...The following program compiles OK on GHC 8.10 but not on GHC 9.0:
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
-- base
import Data.Kind
( Constraint )
--------------------------------------------------------------------------------
data SplineType = Open | Closed
data Curve ( clo :: SplineType ) = Curve {- ... -}
data Spline ( clo :: SplineType ) = Spline {- ... -}
class KnownSplineType ( clo :: SplineType ) where
type TraversalCt clo ( clo' :: SplineType ) :: Constraint
biwitherSpline
:: ( forall clo'. ( TraversalCt clo clo' )
=> Curve clo' -> Maybe ( Curve clo' )
)
-> Spline clo
-> Maybe ( Spline clo )
instance KnownSplineType Open where
type TraversalCt Open clo' = clo' ~ Open
biwitherSpline
:: ( Curve Open -> Maybe ( Curve Open ) )
-> Spline Open
-> Maybe ( Spline Open )
biwitherSpline _ _ = undefined
```
With GHC 9.0, I get the following error:
```
Bug.hs:37:8: error:
* Couldn't match type: Curve 'Open -> Maybe (Curve 'Open)
with: forall (clo' :: SplineType).
TraversalCt 'Open clo' =>
Curve clo' -> Maybe (Curve clo')
Expected: (forall (clo' :: SplineType).
TraversalCt 'Open clo' =>
Curve clo' -> Maybe (Curve clo'))
-> Spline 'Open -> Maybe (Spline 'Open)
Actual: (Curve 'Open -> Maybe (Curve 'Open))
-> Spline 'Open -> Maybe (Spline 'Open)
* When checking that instance signature for `biwitherSpline'
is more general than its signature in the class
Instance sig: (Curve 'Open -> Maybe (Curve 'Open))
-> Spline 'Open -> Maybe (Spline 'Open)
Class sig: (forall (clo' :: SplineType).
TraversalCt 'Open clo' =>
Curve clo' -> Maybe (Curve clo'))
-> Spline 'Open -> Maybe (Spline 'Open)
In the instance declaration for `KnownSplineType 'Open'
|
37 | :: ( Curve Open -> Maybe ( Curve Open ) )
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
```
It seems that GHC 9.0 is unable to use the associated type family instance `TraversalCt Open clo' = clo' ~ Open` in checking that the instance signature is at least as general as the class signature. Is this expected, or an oversight?
Of course, changing the instance signature to the obviously correct
```haskell
biwitherSpline
:: ( forall clo'. ( TraversalCt Open clo' )
=> Curve clo' -> Maybe ( Curve clo' )
)
-> Spline Open
-> Maybe ( Spline Open )
```
makes the program compile again, but I think the other instance signature should also be accepted.https://gitlab.haskell.org/ghc/ghc/-/issues/19432GHC 9.0 rejects default signature that 8.10 accepts2021-03-03T18:29:53ZRyan ScottGHC 9.0 rejects default signature that 8.10 acceptsI originally noticed this issue in the `barbies-2.0.2.0` library on Hackage, which compiles with GHC 8.10.4 but fails to compile on GHC 9.0.1. Here is a minimized version of the code that fails to compile on 9.0.1:
```hs
{-# LANGUAGE Co...I originally noticed this issue in the `barbies-2.0.2.0` library on Hackage, which compiles with GHC 8.10.4 but fails to compile on GHC 9.0.1. Here is a minimized version of the code that fails to compile on 9.0.1:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
import Data.Coerce
import Data.Kind
import Data.Proxy
import GHC.Generics
import GHC.TypeNats
class FunctorT (t :: (k -> Type) -> k' -> Type) where
tmap :: forall f g
. (forall a . f a -> g a)
-> (forall x . t f x -> t g x)
-- Default implementation of 'tmap' based on 'Generic'.
default tmap
:: forall f g
. (forall a . f a -> g a)
-> (forall x. CanDeriveFunctorT t f g x => t f x -> t g x)
tmap f = toP (Proxy @1) . gmap (Proxy @1) f . fromP (Proxy @1)
type CanDeriveFunctorT t f g x
= ( GenericP 1 (t f x)
, GenericP 1 (t g x)
, GFunctor 1 f g (RepP 1 (t f x)) (RepP 1 (t g x))
)
-----
class GFunctor (n :: Nat) f g repbf repbg where
gmap :: Proxy n -> (forall a . f a -> g a) -> repbf x -> repbg x
class
( Coercible (Rep a) (RepP n a)
, Generic a
) => GenericP (n :: Nat) (a :: Type) where
type family RepP n a :: Type -> Type
toP :: Proxy n -> RepP n a x -> a
fromP :: Proxy n -> a -> RepP n a x
```
The important bit is the default signature for `tmap`. With GHC 9.0.1, this is rejected thusly:
```
$ /opt/ghc/9.0.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:24:11: error:
• The default type signature for tmap:
forall (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a)
-> forall (x :: k'). CanDeriveFunctorT t f g x => t f x -> t g x
does not match its corresponding non-default type signature
• When checking the class method:
tmap :: forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *)
(g :: k -> *).
FunctorT t =>
(forall (a :: k). f a -> g a) -> forall (x :: k'). t f x -> t g x
In the class declaration for ‘FunctorT’
|
24 | default tmap
| ^^^^
```
Why does GHC 9.0.1 reject this? According to the [GHC User's Guide section on `DefaultSignatures`](https://downloads.haskell.org/ghc/9.0.1/docs/html/users_guide/exts/default_signatures.html#default-method-signatures):
> The type signature for a default method of a type class must take on the same form as the corresponding main method’s type signature. Otherwise, the typechecker will reject that class’s definition. By “take on the same form”, we mean that the default type signature should differ from the main type signature only in their contexts.
As far as I can tell, `tmap` meets this criterion, as the only difference between the two signatures is the presence of `CanDeriveFunctorT t f g x =>` in the default signature.https://gitlab.haskell.org/ghc/ghc/-/issues/19457conduit-1.3.4 builds with 9.0.1, but not HEAD, due to regression in typecheck...2021-03-09T09:59:21ZRyan Scottconduit-1.3.4 builds with 9.0.1, but not HEAD, due to regression in typechecking sectionsWhile patching `head.hackage` recently, I discovered recently that the `conduit-1.3.4` library fails to build on HEAD, despite compiling with 9.0.1. This is due to a typechecker regression introduced in commit 4196969c53c55191e644d9eb258...While patching `head.hackage` recently, I discovered recently that the `conduit-1.3.4` library fails to build on HEAD, despite compiling with 9.0.1. This is due to a typechecker regression introduced in commit 4196969c53c55191e644d9eb258c14c2bc8467da (`Improve handling of overloaded labels, literals, lists etc`). The issue concerns the way that GHC typechecks left and right sections. Here is a minimized example that illustrates the issue with a right section:
```hs
{-# LANGUAGE RankNTypes #-}
module Bug where
f :: a -> forall b. b -> a
f x _ = x
g :: a -> a
g = (`f` "hello")
```
This compiles on 9.0.1, but fails on HEAD with the following error:
```
$ ~/Software/ghc-9.1.20210227/bin/ghc Bug2.hs
[1 of 1] Compiling Bug2 ( Bug2.hs, Bug2.o )
Bug2.hs:8:6: error:
• Couldn't match type: forall c1. c1 -> String
with: c -> String
Expected: b -> c -> String
Actual: b -> forall c. c -> String
• In the expression: "hello" `j`
In an equation for ‘k’: k = ("hello" `j`)
• Relevant bindings include
k :: b -> c -> String (bound at Bug2.hs:8:1)
|
8 | k = ("hello" `j`)
| ^^^^^^^^^^^
```
It's tempting to say that this should be rejected because of simplified subsumption, but that's not the full story. For one thing, 9.0.1 introduced simplified subsumption, but the code above typechecks under 9.0.1, so this is a HEAD-specific phenomenon. Moreover, [Section 3.5 of the Haskell 2010 Report](https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-300003.5) specifically requires that the following identities hold for sections:
> Translation: The following identities hold:
>
> ```hs
> (op e) = \ x -> x op e
> (e op) = \ x -> e op x
> ```
>
> where `op` is a binary operator, `e` is an expression, and `x` is a variable that does not occur free in `e`.
Therefore, the definition of `g` should be equivalent to:
```hs
g :: a -> a
g = \x -> x `f` "hello"
```
And indeed, that typechecks on both 9.0.1 and HEAD. Therefore, I'm going to deem this a regression, since the Haskell 2010 Report seems to indicate that this ought to work.
The example above uses a right section, but the same issue applies to left sections as well, as shown by this example:
```hs
{-# LANGUAGE RankNTypes #-}
module Bug2 where
j :: a -> b -> forall c. c -> a
j x _ _ = x
k :: b -> c -> String
k = ("hello" `j`)
```
Again, this typechecks on 9.0.1 but not on HEAD:
```
$ ~/Software/ghc-9.1.20210227/bin/ghc Bug2.hs
[1 of 1] Compiling Bug2 ( Bug2.hs, Bug2.o )
Bug2.hs:8:6: error:
• Couldn't match type: forall c1. c1 -> String
with: c -> String
Expected: b -> c -> String
Actual: b -> forall c. c -> String
• In the expression: "hello" `j`
In an equation for ‘k’: k = ("hello" `j`)
• Relevant bindings include
k :: b -> c -> String (bound at Bug2.hs:8:1)
|
8 | k = ("hello" `j`)
| ^^^^^^^^^^^
```
However, the equivalent eta-expanded version of `k` typechecks on both 9.0.1 and HEAD:
```hs
k :: b -> c -> String
k = \x -> "hello" `j` x
```
cc @simonpj9.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/19482"No skolem info" with the infinite kind2022-01-29T16:06:57ZRinat Striungislazybonesxp@gmail.com"No skolem info" with the infinite kind## Summary
Today I get a crash with the following message:
```src/Bug.hs:12:25: error:ghc: panic! (the 'impossible' happened)
(GHC version 9.1.20210210:
No skolem info:
[r_axQl[ssk:1]]
Call stack:
CallStack (from H...## Summary
Today I get a crash with the following message:
```src/Bug.hs:12:25: error:ghc: panic! (the 'impossible' happened)
(GHC version 9.1.20210210:
No skolem info:
[r_axQl[ssk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:181:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Tc/Errors.hs:2847:17 in ghc:GHC.Tc.Errors
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```
## Steps to reproduce
Here is my minimal example to reproduce:
```{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
module Bug where
instance BugClass ((s : sx) :: [r]) where
bugList = testF @r @s
class BugClass k where
bugList :: ()
testF :: forall a (b :: [a]). ()
testF = ()
```
Also, GHC-8.10 works well with a proper error message.
So, it looks like a regression.
## Expected behavior
I should get a compilation error message about the infinite kind construction ( `r ~ [r]`).
## Environment
* GHC version used:
GHC HEAD: [40983d2331fe34c0af6925db7588d5ac6a19ae36](https://gitlab.haskell.org/ghc/ghc/-/tree/40983d2331fe34c0af6925db7588d5ac6a19ae36)9.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/19495Tc trace of checkValidType panics in tcTypeKind for T16391b2022-01-10T23:57:14ZSebastian GrafTc trace of checkValidType panics in tcTypeKind for T16391bIn https://gitlab.haskell.org/ghc/ghc/-/merge_requests/2218#note_335959, I triggered a panic in `tcTypeKind`. I thought that my branch was responsible, but then figured out that without `-ddump-tc-trace`, there was no panic. Then I tried...In https://gitlab.haskell.org/ghc/ghc/-/merge_requests/2218#note_335959, I triggered a panic in `tcTypeKind`. I thought that my branch was responsible, but then figured out that without `-ddump-tc-trace`, there was no panic. Then I tried `-ddump-tc-trace` on `T16391b`:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module T16391b where
import GHC.Exts
type family T (r :: RuntimeRep) :: TYPE r
foo :: T r
foo = foo
```
And sure enough, that panics on HEAD:
```
checkValidTypeghc: panic! (the 'impossible' happened)
(GHC version 9.1.20210305:
tcTypeKind
forall (r :: RuntimeRep). T r
[r_aw2[sk:2]]
T r_aw2[sk:2] :: TYPE r_aw2[sk:2]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:181:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Core/Type.hs:2660:18 in ghc:GHC.Core.Type
```
... when `checkValidType` (I think) ultimately would have printed the following expected error:
```
T16391b.hs:10:8: error:
• Quantified type's kind mentions quantified type variable
type: ‘T 'LiftedRep’
where the body of the forall has this kind: ‘TYPE r’
• In the type signature: foo :: T r
|
10 | foo :: T r
| ^^^
```
It's a matter of printing the error message *before* calling `tcTypeKind`:
```hs
checkValidType ctxt ty
= do { traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (tcTypeKind ty))
; rankn_flag <- xoptM LangExt.RankNTypes
...
; checkNoErrs $
do { check_type ve ty
; checkUserTypeError ty
; traceTc "done ct" (ppr ty) }
...
; traceTc "checkValidType done" (ppr ty <+> text "::" <+> ppr (tcTypeKind ty)) }
```
I suggest we simply delete the ` <+> text "::" <+> ppr (tcTypeKind ty)` of the first `traceTc`.https://gitlab.haskell.org/ghc/ghc/-/issues/19498Typeclass fails to compile with StandaloneKindSignatures; only compiles with ...2021-03-15T11:00:27ZdanidiazTypeclass fails to compile with StandaloneKindSignatures; only compiles with conventional kind annotations## Summary
A typeclass compiles correctly with conventional kind annotations, but when the kinds are given with a standalone kind signature it ceases to compile.
## Steps to reproduce
Try to compile this module:
```
{-# LANGUAGE Allo...## Summary
A typeclass compiles correctly with conventional kind annotations, but when the kinds are given with a standalone kind signature it ceases to compile.
## Steps to reproduce
Try to compile this module:
```
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module Main where
import Data.Kind
import Data.Proxy
import GHC.TypeLits
data Color
= R
| B
deriving (Show, Eq)
data Map symbol q
= E
| N Color (Map symbol q) symbol q (Map symbol q)
deriving (Show, Eq)
type Record :: (q -> Type) -> Map Symbol q -> Type
data Record f t where
Empty :: Record f E
Node :: Record f left -> f v -> Record f right -> Record f (N color left k v right)
type CanMakeBlack :: Map Symbol q -> Constraint
class CanMakeBlack t where
type MakeBlack t :: Map Symbol q
makeBlackR :: Record f t -> Record f (MakeBlack t)
instance CanMakeBlack (N color left k v right) where
type MakeBlack (N color left k v right) = N B left k v right
makeBlackR (Node left fv right) = Node left fv right
instance CanMakeBlack E where
type MakeBlack E = E
makeBlackR Empty = Empty
type Delable :: Symbol -> q -> Map Symbol q -> Constraint
class Delable k v t where
-- Using conventional kind annotations, it compiles correctly
--class Delable (k :: Symbol) (v :: q) (t :: Map Symbol q) where
type Del k v t :: Map Symbol q
del :: Record f t -> Record f (Del k v t)
type Deletable :: Symbol -> q -> Map Symbol q -> Constraint
class Deletable (k :: Symbol) (v :: q) (t :: Map Symbol q) where
type Delete k v t :: Map Symbol q
_delete :: Record f t -> Record f (Delete k v t)
instance (Delable k v t, Del k v t ~ deleted, CanMakeBlack deleted) => Deletable k v t where
type Delete k v t = MakeBlack (Del k v t)
_delete r = makeBlackR (del @_ @k @v r)
main :: IO ()
main = pure ()
```
The compilation will fail with the error:
```
Main.hs:70:15: error:
* Could not deduce: MakeBlack (Del k v t) ~ MakeBlack (Del k v t)
from the context: (Delable k v t, Del k v t ~ deleted,
CanMakeBlack deleted)
bound by the instance declaration at Main.hs:68:10-86
Expected: Record f (Delete k v t)
Actual: Record f (MakeBlack (Del k v t))
NB: `MakeBlack' is a non-injective type family
```
However, if instead of the line
`class Delable k v t where`
We use the line
`class Delable (k :: Symbol) (v :: q) (t :: Map Symbol q) where`
The code compiles correctly, even if the standalone kind signature remains.
## Expected behavior
The code should compile correctly with the standalone kind signature, without need of explicit kind annotations on the variables.
## Environment
* GHC version used: 9.0.1
Optional:
* Operating System: Windows 10https://gitlab.haskell.org/ghc/ghc/-/issues/19503Dead suggestion for -XUnliftedNewtypes in checkNewDataCon2023-09-27T09:55:06ZSebastian GrafDead suggestion for -XUnliftedNewtypes in checkNewDataConNote [Implementation of UnliftedNewtypes], point <Error Messages> says:
```
<Error Messages>: It's tempting to think that the expected kind for a newtype
constructor argument when -XUnliftedNewtypes is *not* enabled should just be Type....Note [Implementation of UnliftedNewtypes], point <Error Messages> says:
```
<Error Messages>: It's tempting to think that the expected kind for a newtype
constructor argument when -XUnliftedNewtypes is *not* enabled should just be Type.
But this leads to difficulty in suggesting to enable UnliftedNewtypes. Here is
an example:
newtype A = MkA Int#
If we expect the argument to MkA to have kind Type, then we get a kind-mismatch
error. The problem is that there is no way to connect this mismatch error to
-XUnliftedNewtypes, and suggest enabling the extension. So, instead, we allow
the A to type-check, but then find the problem when doing validity checking (and
where we get make a suitable error message).
```
I think that Note refers to the code in `GHC.Tc.TyCl.checkNewDataCon` (which is transitively called from `checkValidTyCon`). There we have
```hs
; unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes
; let allowedArgType =
unlifted_newtypes || isLiftedType_maybe (scaledThing arg_ty1) == Just True
; checkTc allowedArgType $ vcat
[ text "A newtype cannot have an unlifted argument type"
, text "Perhaps you intended to use UnliftedNewtypes"
]
```
But that error emssage doesn't occur anywhere in the testsuite. If you try the example `A` from the Note, you instead get
```
test.hs:20:1: error:
• Newtype has non-* return kind ‘TYPE 'IntRep’
Perhaps you intended to use UnliftedNewtypes
• In the newtype declaration for ‘A’
|
20 | newtype A = MkA Int#
| ^^^^^^^^^^^^^^^^^^^^
```
(Side note: It's a bit surprising that the emission of that error suppresses any following errors, for example of a following decl `newtype B = MkB Int#`. Perhaps this has to do with the next paragraph.)
That message (which I actually prefer) is emitted by `GHC.Tc.Gen.HsType.checkDataKindSig`.
It seems we can just get rid of the code in `checkNewDataCon`. Either way, we should update Note [Implementation of UnliftedNewtypes]. Maybe Split if off into its own Sub-Note? That Note is awfully long and has many many sub items.https://gitlab.haskell.org/ghc/ghc/-/issues/19522Levity monomorphic instantiation of unsafeCoerce# is rejected as being levity...2021-10-11T08:15:50ZRyan ScottLevity monomorphic instantiation of unsafeCoerce# is rejected as being levity polymorphic in 9.0+While experimenting with `unsafeCoerce#` recently, I tried the following:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE TypeApplications #-}
module Bug where
import GHC.Exts
import Unsafe.Coerce
f :: Int -> ...While experimenting with `unsafeCoerce#` recently, I tried the following:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE TypeApplications #-}
module Bug where
import GHC.Exts
import Unsafe.Coerce
f :: Int -> Int
f x = unsafeCoerce# @LiftedRep @LiftedRep @Int @Int x
```
Surprisingly, GHC 9.0 and later reject this:
```
$ /opt/ghc/9.0.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:10:7: error:
Cannot use function with levity-polymorphic arguments:
unsafeCoerce# :: forall (q :: RuntimeRep) (r :: RuntimeRep)
(a :: TYPE q) (b :: TYPE r).
a -> b
(Note that levity-polymorphic primops such as 'coerce' and unboxed tuples
are eta-expanded internally because they must occur fully saturated.
Use -fprint-typechecker-elaboration to display the full expression.)
Levity-polymorphic arguments: a :: TYPE q
|
10 | f x = unsafeCoerce# @LiftedRep @LiftedRep @Int @Int x
| ^^^^^^^^^^^^^
```
The error message confuses me, since nothing about this is levity polymorphic.
Note that this only occurs if visible type applications are used. If I remove them:
```hs
f :: Int -> Int
f x = unsafeCoerce# x
```
Then GHC accepts it.9.0.2https://gitlab.haskell.org/ghc/ghc/-/issues/19548Kind generalisation without -XPolyKinds leading to breakage2021-03-17T08:07:24ZSebastian GrafKind generalisation without -XPolyKinds leading to breakageThe following program is reduced from `libraries/Cabal/Cabal/src/Distribution/Utils/Path.hs`, which I didn't manage to compile with @bgamari's [build-cabal.sh script](https://gitlab.haskell.org/bgamari/ghc-utils/-/blob/master/build-cabal...The following program is reduced from `libraries/Cabal/Cabal/src/Distribution/Utils/Path.hs`, which I didn't manage to compile with @bgamari's [build-cabal.sh script](https://gitlab.haskell.org/bgamari/ghc-utils/-/blob/master/build-cabal.sh) today:
```hs
{-# LANGUAGE DeriveDataTypeable #-}
module Path where
import Data.Typeable
class Typeable a => C a where
data T a = T deriving Typeable
instance Typeable a => C (T a)
```
If compiled with HEAD (and `-fprint-explicit-kinds`, this errors
```
Path.hs:9:10: error:
• Could not deduce (Typeable @(*) k)
arising from the superclasses of an instance declaration
from the context: Typeable @k a
bound by the instance declaration at Path.hs:9:10-30
• In the instance declaration for ‘C @{*} (T @{k} a)’
|
9 | instance Typeable a => C (T a)
| ^^^^^^^^^^^^^^^^^^^^^
```
Apparently, `T`'s type parameter has been kind generalised. Why? I don't think `-XDeriveDataTypeable` implies `-XPolyKinds`.
Yet the error message mentions an implicit kind `k` that appears nowhere else in the program.https://gitlab.haskell.org/ghc/ghc/-/issues/19565`plots` fails to typechecking in 9.22021-03-19T23:36:40ZBen Gamari`plots` fails to typechecking in 9.2When updating `head.hackage` for 9.2, I noticed that `plots` now fails to typecheck,
```
src/Plots/Types.hs:697:17: error:
• Reduction stack overflow; size = 201
When simplifyin...When updating `head.hackage` for 9.2, I noticed that `plots` now fails to typecheck,
```
src/Plots/Types.hs:697:17: error:
• Reduction stack overflow; size = 201
When simplifying the following type: V p1
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 pattern: StyledPlot p opts sty
In an equation for ‘styledPlot’:
styledPlot f s@(StyledPlot p opts sty)
= case eq p of
Just Refl -> f p <&> \ p' -> StyledPlot p' opts sty
Nothing -> pure s
where
eq :: Typeable a => a -> Maybe (a :~: p)
eq _ = eqT
|
697 | styledPlot f s@(StyledPlot p opts sty) =
| ^^^^^^^^^^^^^^^^^^^^^
```
I haven't tried lifting the reduction depth yet.9.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/19668Exponential blowup in T9198 (regresssion from 8.10 and 9.0)2021-10-11T08:17:53ZvdukhovniExponential blowup in T9198 (regresssion from 8.10 and 9.0)## Summary
The T9198 test is showing rather unstable metrics in head, but the real issue is not the wobbly numbers but the scale. In GHC 8.10.4 and 9.0.1, adding more continuation terms results in linear cost increases, but with head t...## Summary
The T9198 test is showing rather unstable metrics in head, but the real issue is not the wobbly numbers but the scale. In GHC 8.10.4 and 9.0.1, adding more continuation terms results in linear cost increases, but with head the cost doubles with every term, as reported in https://gitlab.haskell.org/ghc/ghc/-/merge_requests/4890#note_343948
## Steps to reproduce
Compile `testsuite/tests/perf/compiler/T9198.hs` with `+RTS -s` with varying numbers of additional `a` continuation terms. The GHC runtime and memory allocation grow exponentially. The same is not observed with GHC 8.10.4 for example.
## Expected behavior
Linear cost. With 8.10.4 and the continuation count unmodified I get:
```
$ ghc -O -fasm testsuite/tests/perf/compiler/T9198.hs +RTS -s
116,102,480 bytes allocated in the heap
...
MUT time 0.069s ( 0.572s elapsed)
GC time 0.111s ( 0.111s elapsed)
Total time 0.181s ( 0.689s elapsed)
```
With head I get:
```
514,989,696 bytes allocated in the heap
...
MUT time 0.212s ( 0.604s elapsed)
GC time 0.366s ( 0.366s elapsed)
Total time 0.581s ( 0.979s elapsed)
```
## Environment
* GHC version used: head (9.1.20210402)9.2.1Matthew PickeringMatthew Pickeringhttps://gitlab.haskell.org/ghc/ghc/-/issues/19677GHC does not rewrite in FunTy2022-02-21T17:09:27ZRichard Eisenbergrae@richarde.devGHC does not rewrite in FunTyConsider
```hs
{-# LANGUAGE ExplicitForAll, PolyKinds, DataKinds, TypeFamilies, GADTs #-}
module Bug where
import GHC.Exts
class C x where
meth :: x -> ()
instance C (a -> b) where
meth _ = ()
type family Lifty throttle where
...Consider
```hs
{-# LANGUAGE ExplicitForAll, PolyKinds, DataKinds, TypeFamilies, GADTs #-}
module Bug where
import GHC.Exts
class C x where
meth :: x -> ()
instance C (a -> b) where
meth _ = ()
type family Lifty throttle where
Lifty Int = LiftedRep
data G a where
MkG :: G Int
foo :: forall i (a :: TYPE (Lifty i)) (b :: TYPE (Lifty i)). G i -> (a -> b) -> ()
foo MkG = meth
```
GHC rejects, saying it cannot find an instance for `C (a -> b)`. But it should accept.
The problem is that the kinds of `a` and `b` are `TYPE (Lifty i)`. Even if we know `i ~ Int`, and therefore that `Lifty i ~ LiftedRep`, GHC does not rewrite these kinds internally, allowing instance matching to succeed.
!2477, when complete, should address this.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/19682Constraint solver regression in 9.22021-07-28T16:20:14ZAndres LöhConstraint solver regression in 9.2## Summary
While trying to make the `generics-sop` and `sop-core` packages compatible with GHC 9.2, I discovered a regression in the constraint solver. The included program compiles at with GHC 9.0.1, GHC 8.8.4, GHC 8.6.5, GHC 8.4.4, GH...## Summary
While trying to make the `generics-sop` and `sop-core` packages compatible with GHC 9.2, I discovered a regression in the constraint solver. The included program compiles at with GHC 9.0.1, GHC 8.8.4, GHC 8.6.5, GHC 8.4.4, GHC 8.2.2, but it fails with GHC 9.2 with the following error message:
```
AllEq.hs:19:21: error:
• Couldn't match type ‘ys0’ with ‘Head ys0 : Tail ys0’
arising from a use of ‘convert’
• In the second argument of ‘const’, namely ‘(convert xs)’
In the expression: const () (convert xs)
In an equation for ‘test’: test xs = const () (convert xs)
|
19 | test xs = const () (convert xs)
| ^^^^^^^
```
## Steps to reproduce
Run `ghc` or `ghci` on the following file:
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module AllEq where
import Data.Kind
import Data.Proxy
convert :: (AllEq xs ys) => Proxy xs -> Proxy ys
convert p = Proxy
-- Works with ghc up to 9.0. Fails with ghc 9.2.
test :: Proxy '[Char, Bool] -> ()
test xs = const () (convert xs)
class (AllEqF xs ys, SameShapeAs xs ys) => AllEq (xs :: [a]) (ys :: [a])
instance (AllEqF xs ys, SameShapeAs xs ys) => AllEq xs ys
type family SameShapeAs (xs :: [a]) (ys :: [a]) :: Constraint where
SameShapeAs '[] ys = (ys ~ '[])
SameShapeAs (x : xs) ys = (ys ~ (Head ys : Tail ys))
type family AllEqF (xs :: [a]) (ys :: [a]) :: Constraint where
AllEqF '[] '[] = ()
AllEqF (x : xs) (y : ys) = (x ~ y, AllEq xs ys)
type family Head (xs :: [a]) :: a where
Head (x : xs) = x
type family Tail (xs :: [a]) :: [a] where
Tail (x : xs) = xs
```
## Expected behavior
I would expect the program to be accepted.
## Environment
* GHC version used: 9.2.0.20210406, built locally on my machine from the `ghc-9.2` branch at commit d197fb3d5c053cfb526272c29a443c33d1af0980
Optional:
* Operating System: Linux (NixOS)
* System Architecture: x86_649.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/19690Bottom dictionaries can be derived with QuantifiedConstraints, UndecidableIns...2023-01-26T04:02:51Zaadaa-fgtaaBottom dictionaries can be derived with QuantifiedConstraints, UndecidableInstances and UndecidableSuperClasses[I'm not sure if this is a bug or documentation issue. I'd prefer the former so I applied "bug" template]
## Summary
With `QuantifiedConstraints`, `UndecidableInstances` and `UndecidableSuperClasses` it is possible to
produce bottom di...[I'm not sure if this is a bug or documentation issue. I'd prefer the former so I applied "bug" template]
## Summary
With `QuantifiedConstraints`, `UndecidableInstances` and `UndecidableSuperClasses` it is possible to
produce bottom dictionary, which isn't mentioned in docs as far as I can see.
## Steps to reproduce
```haskell
{-# LANGUAGE UndecidableInstances, UndecidableSuperClasses, ConstraintKinds, FlexibleInstances,
GADTs, QuantifiedConstraints, TypeApplications, ScopedTypeVariables #-}
module QCLoop where
class c => Hold c
instance c => Hold c
data Dict c = c => Dict
anythingDict :: Dict c
anythingDict = go
where
go :: (Hold c => c) => Dict c
go = Dict
```
Produces bottom dictionary
```haskell
Rec {
$dHold_rxi :: forall {c :: Constraint}. Hold c
$dHold_rxi = $dHold_rxi
end Rec }
anythingDict :: forall (c :: Constraint). Dict c
anythingDict = \ (@c) -> Dict ($dHold_rxi `cast` <Co:2>)
```
## Expected behavior
Either the program is rejected with "could not deduce c" or "too many iterations", or documentation for
`UndecidableInstances` and/or `UndecidableSuperClasses` mentions that they may result in
non-termination not only in typechecker but also at runtime.
I would really prefer the former as the ability to "prove" anything with such code scares me a bit.
## Environment
* GHC version used: 8.10.4, 9.0.1 and 9.1.20210409
* Operating System: Linux (NixOS)
* System Architecture: x86-64https://gitlab.haskell.org/ghc/ghc/-/issues/19728GHC 9.0+ fails to combine levity-polymorphic newtype constructor with TypeApp...2021-04-22T18:08:29ZRyan ScottGHC 9.0+ fails to combine levity-polymorphic newtype constructor with TypeApplicationsGHC 8.10.4 has no problem typechecking this program:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeAppl...GHC 8.10.4 has no problem typechecking this program:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UnliftedNewtypes #-}
module Bug where
import GHC.Exts
type Id :: TYPE r -> TYPE r
newtype Id a where
MkId :: forall r (a :: TYPE r). a -> Id a
idBool :: Id Bool
idBool = MkId @LiftedRep @Bool True
```
However, GHC 9.0.1 and later fail with:
```
$ /opt/ghc/9.0.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:17:10: error:
• Cannot apply expression of type ‘a0 -> Id a0’
to a visible type argument ‘LiftedRep’
• In the expression: MkId @LiftedRep @Bool True
In an equation for ‘idBool’: idBool = MkId @LiftedRep @Bool True
|
17 | idBool = MkId @LiftedRep @Bool True
| ^^^^^^^^^^^^^^^^^^^^^^^^^^
```
As far as I can tell, this program should be expected to typecheck, so I believe this is a regression.https://gitlab.haskell.org/ghc/ghc/-/issues/19847Type application in pattern does not substitute correctly2023-02-09T17:22:09ZRichard Eisenbergrae@richarde.devType application in pattern does not substitute correctlySee also
* #19577
* #22383
* #21501
Inspired by @Icelandjack's https://gitlab.haskell.org/ghc/ghc/-/issues/19691#note_352594, I typed in
```hs
pattern Is :: forall (b :: Type) (a :: Type). Typeable b => (a ~ b) => TypeRep a
pattern Is ...See also
* #19577
* #22383
* #21501
Inspired by @Icelandjack's https://gitlab.haskell.org/ghc/ghc/-/issues/19691#note_352594, I typed in
```hs
pattern Is :: forall (b :: Type) (a :: Type). Typeable b => (a ~ b) => TypeRep a
pattern Is <- (eqTypeRep (typeRep @b) -> Just HRefl)
where Is = typeRep
def :: TypeRep a -> a
def = \case
Is @Int -> 10
Is @Bool -> False
```
which looks pretty sensible to me. HEAD tells me
```
Scratch.hs:40:3: error:
• No instance for (Typeable b0) arising from a use of ‘Is’
• In the pattern: Is @Int
In a case alternative: Is @Int -> 10
In the expression:
\case
Is @Int -> 10
Is @Bool -> False
|
40 | Is @Int -> 10
| ^^^^^^^
Scratch.hs:40:3: error:
• Could not deduce: a ~ Int
from the context: a ~ b0
bound by a pattern with pattern synonym:
Is :: forall b a. Typeable b => (a ~ b) => TypeRep a,
in a case alternative
at Scratch.hs:40:3-9
Expected: b0
Actual: Int
‘a’ is a rigid type variable bound by
the type signature for:
def :: forall a. TypeRep a -> a
at Scratch.hs:38:1-21
• In the pattern: Is @Int
In a case alternative: Is @Int -> 10
In the expression:
\case
Is @Int -> 10
Is @Bool -> False
• Relevant bindings include
def :: TypeRep a -> a (bound at Scratch.hs:39:1)
|
40 | Is @Int -> 10
| ^^^^^^^
Scratch.hs:41:3: error:
• No instance for (Typeable b1) arising from a use of ‘Is’
• In the pattern: Is @Bool
In a case alternative: Is @Bool -> False
In the expression:
\case
Is @Int -> 10
Is @Bool -> False
|
41 | Is @Bool -> False
| ^^^^^^^^
Scratch.hs:41:15: error:
• Could not deduce: a ~ Bool
from the context: a ~ b1
bound by a pattern with pattern synonym:
Is :: forall b a. Typeable b => (a ~ b) => TypeRep a,
in a case alternative
at Scratch.hs:41:3-10
‘a’ is a rigid type variable bound by
the type signature for:
def :: forall a. TypeRep a -> a
at Scratch.hs:38:1-21
• In the expression: False
In a case alternative: Is @Bool -> False
In the expression:
\case
Is @Int -> 10
Is @Bool -> False
• Relevant bindings include
def :: TypeRep a -> a (bound at Scratch.hs:39:1)
|
41 | Is @Bool -> False
|
```
But that looks wrong: it shouldn't be looking for `Typeable b0` or `Typeable b1`, it should be looking for `Typeable Int` or `Typeable Bool`. While I have not investigated further, this smells like a missing application of a substitution somewhere.https://gitlab.haskell.org/ghc/ghc/-/issues/20009Degradation in error message clarity for ` GHC.TypeNats.<=?`2022-07-28T21:32:40ZChristiaan BaaijDegradation in error message clarity for ` GHC.TypeNats.<=?`## Summary
With the introduction of https://gitlab.haskell.org/ghc/ghc/-/commit/eea96042f1e8682605ae68db10f2bcdd7dab923e the clarity of error messages involving `GHC.TypeNats.<=?` has degraded compared to GHC 9.0.1 or earlier.
## Steps...## Summary
With the introduction of https://gitlab.haskell.org/ghc/ghc/-/commit/eea96042f1e8682605ae68db10f2bcdd7dab923e the clarity of error messages involving `GHC.TypeNats.<=?` has degraded compared to GHC 9.0.1 or earlier.
## Steps to reproduce
Given this code `TestInEq.hs`:
```haskell
{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators #-}
module TestInEq where
import Data.Proxy
import GHC.TypeLits
proxyInEq :: (a <= b) => Proxy a -> Proxy b -> ()
proxyInEq _ _ = ()
proxyInEq1 :: Proxy a -> Proxy (a+1) -> ()
proxyInEq1 = proxyInEq
```
## Expected behavior
On GHC 9.0.1 and prior, one would get the error message:
```
$ ghci TestInEq.hs
GHCi, version 9.0.1: https://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling TestInEq ( TestInEq.hs, interpreted )
TestInEq.hs:11:14: error:
• Couldn't match type ‘a <=? (a + 1)’ with ‘'True’
arising from a use of ‘proxyInEq’
• In the expression: proxyInEq
In an equation for ‘proxyInEq1’: proxyInEq1 = proxyInEq
• Relevant bindings include
proxyInEq1 :: Proxy a -> Proxy (a + 1) -> ()
(bound at TestInEq.hs:11:1)
|
11 | proxyInEq1 = proxyInEq
| ^^^^^^^^^
Failed, no modules loaded.
ghci>
```
But on GHC 9.2.0.20210422, which includes https://gitlab.haskell.org/ghc/ghc/-/commit/eea96042f1e8682605ae68db10f2bcdd7dab923e, one gets the following error message
```
$ ghci TestInEq.hs
GHCi, version 9.2.0.20210422: https://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling TestInEq ( TestInEq.hs, interpreted )
TestInEq.hs:11:14: error:
• Couldn't match type ‘Data.Type.Ord.OrdCond
(CmpNat a (a + 1)) 'True 'True 'False’
with ‘'True’
arising from a use of ‘proxyInEq’
• In the expression: proxyInEq
In an equation for ‘proxyInEq1’: proxyInEq1 = proxyInEq
• Relevant bindings include
proxyInEq1 :: Proxy a -> Proxy (a + 1) -> ()
(bound at TestInEq.hs:11:1)
|
11 | proxyInEq1 = proxyInEq
| ^^^^^^^^^
Failed, no modules loaded.
ghci>
```
which I feel is far less clear.
At the least, I hope we can recover the error message of GHC 9.0.1 or earlier. And it would be even nicer if this could be fixed before the GHC 9.2.1 release. I can envision at least three possible solutions:
1. Reinstate `(GHC.TypeNats.<=?) :: Nat -> Nat -> Bool` as a builtin type family
2. Somehow add a custom type-error to `Data.Type.Ord.OrdCond`
3. Don't expand type aliases in type errors
Following up on 3, it would be even nicer if we could actually get an error along the lines of:
```
TestInEq.hs:11:14: error:
• Couldn't satisfy ‘a <= (a + 1)’
arising from a use of ‘proxyInEq’
• In the expression: proxyInEq
In an equation for ‘proxyInEq1’: proxyInEq1 = proxyInEq
• Relevant bindings include
proxyInEq1 :: Proxy a -> Proxy (a + 1) -> ()
(bound at TestInEq.hs:11:1)
|
11 | proxyInEq1 = proxyInEq
| ^^^^^^^^^
```
where the type synonym `(GHC.TypeNats.<=) :: Nat -> Nat -> Constraint` isn't expanded either.
This issue was/is also discussed at: https://mail.haskell.org/pipermail/ghc-devs/2021-June/019992.html
## Environment
* GHC version used: 9.2.0.20210422https://gitlab.haskell.org/ghc/ghc/-/issues/20063No skolem info panic involving typed hole2022-03-22T09:20:15Zsheafsam.derbyshire@gmail.comNo skolem info panic involving typed holeThe following program causes a `No skolem info` panic on GHC 9.0.1, 9.2.1, HEAD, but not on GHC 8.10.5.
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds ...The following program causes a `No skolem info` panic on GHC 9.0.1, 9.2.1, HEAD, but not on GHC 8.10.5.
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
data Context where
Extend :: forall k. Context -> Context
type (:*&) :: Context -> forall k -> Context
type ctx :*& k = Extend @k ctx
data Idx ctx where
T :: Idx ctx -> Idx (ctx :*& l)
data Rn ctx1 ctx2 where
U :: Rn ctx1 ctx2 -> Rn (ctx1 :*& l) (ctx2 :*& l)
rnRename :: Rn ctx1 ctx2 -> Idx ctx3 -> Idx ctx4
rnRename (U _ ) _ = T _
rnRename _ T = undefined
```
```
[1 of 1] Compiling Bug ( src\Bug.hs, interpreted )
ghc.exe: panic! (the 'impossible' happened)
(GHC version 9.0.1:
No skolem info:
[ctx4_aBB[sk:1]]
```
The program should be rejected, and the error given with GHC 8.10.5 seems perfect:
```
[1 of 1] Compiling Bug ( src\Bug.hs, interpreted )
src\Bug.hs:26:17: error:
• The constructor ‘T’ should have 1 argument, but has been given none
• In the pattern: T
In an equation for ‘rnRename’: rnRename _ T = undefined
|
26 | rnRename _ T = undefined
| ^
```
The issue seems to be related to the presence of a typed hole on the line prior to the bogus pattern match.https://gitlab.haskell.org/ghc/ghc/-/issues/20161Use a specific Reduction datatype instead of `(Type,Coercion)`2021-08-05T08:14:00Zsheafsam.derbyshire@gmail.comUse a specific Reduction datatype instead of `(Type,Coercion)`As I discovered in !5909, introducing a datatype `data Reduction = Reduction Coercion !Type` for use in the rewriter, replacing pairs `(Type, Coercion)` has several benefits:
* improved performance in rewriting of type families (aro...As I discovered in !5909, introducing a datatype `data Reduction = Reduction Coercion !Type` for use in the rewriter, replacing pairs `(Type, Coercion)` has several benefits:
* improved performance in rewriting of type families (around 2.5% improvement in `T9872`),
* improved consistency around orientation of rewritings, as a `Reduction` is always left-to-right (the coercion's RHS type is always the type stored in the 'Reduction').
@rae suggested that this could be taken much further. His idea is to introduce combinators that work purely on the level of `Reduction`s, e.g. `mkReflRedn`, `mkTransRedn`, `mkTyConAppRedn`, etc. This means that other parts of the code won't have to worry about getting the orientations right (e.g. whether to use `mkCoherenceRightCo` or `mkCoherenceLeftCo`).sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/20227Deferred type errors are too lazy, and can be dropped by Core optimisations2021-08-14T11:28:35Zsheafsam.derbyshire@gmail.comDeferred type errors are too lazy, and can be dropped by Core optimisationsThe mechanism for deferring type errors doesn't force the errors, meaning that programs that should fail with a deferred type error at runtime can be run without any errors. Consider the following example (from @rae):
```haskell
{-# LAN...The mechanism for deferring type errors doesn't force the errors, meaning that programs that should fail with a deferred type error at runtime can be run without any errors. Consider the following example (from @rae):
```haskell
{-# LANGUAGE FlexibleContexts #-}
{-# OPTIONS_GHC -fdefer-type-errors #-}
module Main where
h :: Show (Int -> Int) => Int -> Int
h x = x
j :: Int
j = h 5
main :: IO ()
main = print j
```
```
./Main
5
```
This program runs without error, when one would have expected a type error about a missing `Show (Int -> Int)` instance. Richard points out that this can be a genuine security concern, for instance if constraints are used to ensure certain preconditions; a code-path that contains a type error can get run anyway!
The crux of the matter is that the evidence for `Show (Int -> Int)` is lifted:
```haskell
h :: Show (Int -> Int) => Int -> Int
h = \ ($dShow :: Show (Int -> Int)) (x :: Int) -> x
j :: Int
j = let {
$dShow :: Show (Int -> Int)
$dShow
= typeError @LiftedRep @(Show (Int -> Int))
"error:\n\
\ * No instance for (Show (Int -> Int)) arising from a use of `h'\n\
\ (maybe you haven't applied a function to enough arguments?)\n\
\ * In the expression: h 5\n\
\ In an equation for `j': j = h 5\n\
\(deferred type error)"# } in
h $dShow (I# 5#)
```
As `$dShow` is not forced in `j`, and is unused in `h`, Core optimisations drop the type error, resulting in
```haskell
j :: Int
j = I# 5#
```
Note that this problem doesn't arise for equality constraints, because their evidence is unlifted. For instance:
```haskell
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# OPTIONS_GHC -fdefer-type-errors #-}
module Main where
h2 :: Int ~ Bool => Int -> Int
h2 x = x
j2 :: Int
j2 = h2 5
main :: IO ()
main = print j2
```
```
./Main
Main: Main.hs:11:6: error:
* Couldn't match type `Int' with `Bool' arising from a use of `h2'
* In the expression: h2 5
In an equation for `j2': j2 = h2 5
(deferred type error)
```
This is because `Int ~# Bool` is unlifted, meaning that we must `case` on it in Core:
```haskell
h2 :: (Int ~ Bool) => Int -> Int
h2 = \ ($d~:: Int ~ Bool) (x :: Int) -> x
j2 :: Int
j2
= case typeError @(TupleRep []) @(Int ~# Bool)
"error:\n\
\ * Couldn't match type `Int' with `Bool' arising from a use of `h2'\n\
\ * In the expression: h2 5\n\
\ In an equation for `j2': j2 = h2 5\n\
\(deferred type error)"#
of co
{ __DEFAULT ->
let {
$d~ :: Int ~ Bool
[LclId]
$d~
= Eq# @Type @Int @Bool @~(co :: Int ~# Bool) } in
h2 $d~ (I# 5#)
}
```
Notice the `case` statement on the `typeError`, instead of the `let` binding we saw in the previous example.
Richard suggested that we should make constraints unlifted (e.g. `Constraint ~ TYPE (BoxedRep Unlifted)` in Core), or, barring that, otherwise ensure that the evidence has been evaluated.
Note also that enabling `-fdicts-strict` does not make a difference to the issue reported here.
See also #11197 for the opposite issue (deferred type errors being evaluated too eagerly).https://gitlab.haskell.org/ghc/ghc/-/issues/20231mightEqualLater finds an unbound cbv2022-05-09T08:14:55ZYellPikamightEqualLater finds an unbound cbv## Summary
The file [Bug.hs](/uploads/36f2dbf05c57a71ca48bea1265bb9d10/Bug.hs) produces
```haskell
{-# LANGUAGE
DataKinds,
GADTs,
QuantifiedConstraints,
TypeFamilies
#-}
module Bug where
type family Foo x where
Fo...## Summary
The file [Bug.hs](/uploads/36f2dbf05c57a71ca48bea1265bb9d10/Bug.hs) produces
```haskell
{-# LANGUAGE
DataKinds,
GADTs,
QuantifiedConstraints,
TypeFamilies
#-}
module Bug where
type family Foo x where
Foo (Maybe a) = a
data Bug1 a b c where
Bug1 :: (a ~ 'True => Show b, a ~ 'False => Show c) => Bug1 a b c
data Bug2 f a b where
Bug2 :: (a ~ 'True => f b) => Bug2 f a b
bug :: b ~ Maybe (Foo b) => Bug2 Show a (Foo b) -> Bug1 a (Foo b) Int
bug Bug2 = Bug1
```
```
ghc: panic! (the 'impossible' happened)
(GHC version 9.2.0.20210422:
mightEqualLater finds an unbound cbv
cbv_aLN[cbv:1]
[]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:181:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Tc/Solver/Monad.hs:2558:16 in ghc:GHC.Tc.Solver.Monad
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```
## Steps to reproduce
Run `ghci Bug`.
## Expected behavior
File should type check successfully.
## Environment
* GHC version used: 9.2.1-alpha2 (9.2.0.20210422)
Optional:
* Operating System: Arch Linux
* System Architecture: x86-649.2.2https://gitlab.haskell.org/ghc/ghc/-/issues/20277Representation-polymorphic unboxed sum causes a panic2021-10-18T10:52:12Zsheafsam.derbyshire@gmail.comRepresentation-polymorphic unboxed sum causes a panicThe existing representation-polymorphism checks allow some unboxed sums to slip through the cracks:
```haskell
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UnboxedTuples #-}
mo...The existing representation-polymorphism checks allow some unboxed sums to slip through the cracks:
```haskell
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UnboxedTuples #-}
module RepPolySum where
import GHC.Exts
baz :: forall (rep :: RuntimeRep) (a :: TYPE rep). () -> (# Int# | a #)
baz _ = (# 17# | #)
```
```
ghc: panic! (the 'impossible' happened)
(GHC version 9.0.1:
runtimeRepPrimRep
typePrimRep (a_aCt :: TYPE rep_aCs)
rep_aCs
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler\GHC\Utils\Outputable.hs:1230:37 in ghc:GHC.Utils.Outputable
pprPanic, called at compiler\\GHC\\Types\\RepType.hs:527:5 in ghc:GHC.Types.RepType
```
(That's with GHC 9.0; the same error exists on HEAD.)
It wouldn't be hard to fix with the existing mechanisms (in the desugarer), but I'm currently fixing it in the typechecker as part of !6164.https://gitlab.haskell.org/ghc/ghc/-/issues/20330Representation-polymorphism checks for primops check too many arguments2021-10-18T10:52:12Zsheafsam.derbyshire@gmail.comRepresentation-polymorphism checks for primops check too many argumentsThe following program is currently rejected:
```haskell
blart :: forall (r :: RuntimeRep) (a :: TYPE r). a -> a
blart = raise# 5
```
```
error:
Cannot use function with representation-polymorphic arguments:
raise# :: Integer ...The following program is currently rejected:
```haskell
blart :: forall (r :: RuntimeRep) (a :: TYPE r). a -> a
blart = raise# 5
```
```
error:
Cannot use function with representation-polymorphic arguments:
raise# :: Integer -> a -> a
(Note that representation-polymorphic primops,
such as 'coerce' and unboxed tuples, are eta-expanded
internally because they must occur fully saturated.
Use -fprint-typechecker-elaboration to display the full expression.)
Representation-polymorphic arguments: a :: TYPE r
|
13 | blart = raise# 5
| ^^^^^^
```
The problem is that the code that checks for disallowed representation-polymorphism when instantiating primops, which is supposed to catch cases like:
```haskell
foo :: forall (r :: RuntimeRep) (a :: TYPE r) b. a -> b
foo = unsafeCoerce#
```
ends up checking all the function arguments in the return type, even past the primop's arity.
I will be fixing this as part of !6164.https://gitlab.haskell.org/ghc/ghc/-/issues/20356Constraint-vs-Type causes a panic2021-10-22T17:00:34ZRichard Eisenbergrae@richarde.devConstraint-vs-Type causes a panic@monoidal observes in https://gitlab.haskell.org/ghc/ghc/-/issues/11715#note_375240 that
```hs
{-# LANGUAGE TypeFamilies, PolyKinds, ConstraintKinds #-}
import GHC.Types
type family Id (a :: k -> Constraint) :: l -> Constraint
type inst...@monoidal observes in https://gitlab.haskell.org/ghc/ghc/-/issues/11715#note_375240 that
```hs
{-# LANGUAGE TypeFamilies, PolyKinds, ConstraintKinds #-}
import GHC.Types
type family Id (a :: k -> Constraint) :: l -> Constraint
type instance Id f = f
type T :: Constraint -> Constraint
type T = Id Eq
data Proxy p = MkProxy
id' :: f a -> f a
id' x = x
z = id' (MkProxy @T)
```
causes
```
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.3.20210824:
ASSERT failed!
Ill-kinded update to meta tyvar
a_aIJ[tau:1] :: Constraint -> Constraint
Constraint -> Constraint := Eq :: * -> Constraint
Call stack:
CallStack (from HasCallStack):
massertPpr, called at compiler/GHC/Tc/Utils/TcMType.hs:1009:10 in ghc:GHC.Tc.Utils.TcMType
```
when assertions are enabled (e.g. a `DEBUG` compiler).
Constraint-vs-Type is a difficult problem (see #11715), but I think we can pull this off and fix it. I imagine we just need to change an `eqType` to `tcEqType` somewhere.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/20363Newtype over fully applied Levity Polymorphic Type family gives Levity Polymo...2022-03-14T19:08:37ZTarmeanNewtype over fully applied Levity Polymorphic Type family gives Levity Polymorphism error## Summary
If an UnliftedNewtype wraps a (kind-polymorphic) fully reducable type family it still gives a levity-polymorphism error when used. However the concrete type is known at the callsite and not actually polymorphic.
## Steps to...## Summary
If an UnliftedNewtype wraps a (kind-polymorphic) fully reducable type family it still gives a levity-polymorphism error when used. However the concrete type is known at the callsite and not actually polymorphic.
## Steps to reproduce
Here is some example code:
```
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UnboxedTuples #-}
{-# LANGUAGE UnliftedNewtypes #-}
module Scratch where
import GHC.Exts
-- I'm not sure how to give this type with explicit arguments
type ListTyp :: forall (n::ANat) (k::RuntimeRep) (a :: TYPE k). TYPE (ListRep n k)
type family ListTyp where
ListTyp @ANil = (# #)
ListTyp @(ASuc n) @k @a = (# a, ListTyp @n @k @a #)
type family ListRep (n :: ANat) (a::RuntimeRep) where
ListRep ANil _ = (TupleRep '[])
ListRep (ASuc s) a = (TupleRep '[a, ListRep s a])
data ANat = ANil | ASuc ANat
newtype UnpackedVec (n :: ANat) (k :: RuntimeRep) (a :: TYPE k) = UV (ListTyp @n @k @a)
```
These work (unsurprisingly):
`````
rawTup :: (# #) -> Int
rawTup (# #) = 0
typeFamTup :: ListTyp @'ANil @LiftedRep @Int -> Int
typeFamTup (# #) = 0
`````
This breaks:
`````
newtypeFam :: UnpackedVec 'ANil LiftedRep Int -> Int
newtypeFam (UV (# #)) = 0
-- [typecheck] [E] A levity-polymorphic type is not allowed here:
-- Type: ListTyp
-- Kind: TYPE (ListRep 'ANil 'LiftedRep)
-- In a wildcard pattern
`````
But an Identity newtype over the type family compiles:
`````
newtype SIdentity (k :: TYPE a) = SIdentity k
type UnpackedVecI (n :: ANat) (k :: RuntimeRep) (a :: TYPE k) = SIdentity (ListTyp @n @k @a)
newtypeFamSyn :: UnpackedVecI 'ANil LiftedRep Int -> Int
newtypeFamSyn (SIdentity (# #)) = 0
`````
## Expected behavior
Expected Behavior: If the code typechecks without newtype then my intuition was that adding a newtype with -XUnliftedNewtypes should keep working.
## Motivation
I think the code is weird enough that it needs some motivation.
I am currently trying to compare how various data representations - under IORef, strict, unpacked, unlifted, etc - affect performance for mutable data structures. I mostly use an identical implementation and switch behavior via type aliases to pick operations. Because the call sites are all concrete I wondered whether typefamily-build type representations were usable if type family reduces. That part works! But a newtype over the type family breaks.
Fixing this very well might not be worth the implementation cost since it isn't possible to write polymorphic functions either way. Long term I could see some usefulness via something like Kotlin's (macro-like) approach to inline functions. If the unoptimized code is copy-pasted to every callsite then levity polymorphism should be fine because it won't be polymorphic at the callsite, right?
## Environment
* GHC version used: 8.10.4 and 9.2.1-alpha2sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/20396Backpack does not support -ddump-tc-trace2021-10-14T09:21:15Zsheafsam.derbyshire@gmail.comBackpack does not support -ddump-tc-traceWhile working on !6164 I have needed to debug the typechecker in backpack specific scenarios, and it has been a bit of a nightmare because there is no way to enable `-ddump-tc-trace` when compiling `.bkp` files using `--backpack`.While working on !6164 I have needed to debug the typechecker in backpack specific scenarios, and it has been a bit of a nightmare because there is no way to enable `-ddump-tc-trace` when compiling `.bkp` files using `--backpack`.https://gitlab.haskell.org/ghc/ghc/-/issues/20408Make `eqTypeIO` that sees through type families2021-10-04T05:42:12ZZiyang Liuunsafefixio@gmail.comMake `eqTypeIO` that sees through type families<!--
READ THIS FIRST: If the feature you are proposing changes the language that GHC accepts
or adds any warnings to `-Wall`, it should be written as a [GHC Proposal](https://github.com/ghc-proposals/ghc-proposals/).
Other features, appr...<!--
READ THIS FIRST: If the feature you are proposing changes the language that GHC accepts
or adds any warnings to `-Wall`, it should be written as a [GHC Proposal](https://github.com/ghc-proposals/ghc-proposals/).
Other features, appropriate for a GitLab feature request, include GHC API/plugin
innovations, new low-impact compiler flags, or other similar additions to GHC.
-->
## Motivation
In my experience, the fact that `eqType` only sees through type synonyms, but not type families, severely limits its usefulness.
It _seems_ that it should be possible to implement `eqTypeIO` that sees through type families, via `rewrite_fam_app` and `runTcInteractive`, although I haven't studied the details.
The type would be something like `eqTypeIO :: HscEnv -> Type -> Type -> IO Bool` (or a different monad, if `IO` is not a good fit).
## Proposal
Implement `eqTypeIO`, if possible.https://gitlab.haskell.org/ghc/ghc/-/issues/20443Type application in patterns ignores inferredness of type variables2022-10-29T14:21:41ZJakob BrünkerType application in patterns ignores inferredness of type variables## Summary
When a constructor has inferred arguments, like `k` in `Proxy :: forall {k} (t :: k). Proxy t`, type application in patterns (!2464) treats the `k` as though it were not inferred.
## Steps to reproduce
```haskell
import Dat...## Summary
When a constructor has inferred arguments, like `k` in `Proxy :: forall {k} (t :: k). Proxy t`, type application in patterns (!2464) treats the `k` as though it were not inferred.
## Steps to reproduce
```haskell
import Data.Kind
data Proxy t where
Proxy :: forall {k} (t :: k) . Proxy t
a :: () -> Proxy Int
-- a = Proxy @Type @Int -- This would, rightfully, not compile
a () = Proxy @Int
b :: Proxy Int -> ()
b (Proxy @Type @Int) = () -- This compiles, but shouldn't
b (Proxy @Int) = () -- This should compile, but doesn't
{--
TypeAppBug.hs:13:4: error:
* Expected a type, but found something with kind `Int'
* In the pattern: Proxy @Int
In an equation for `b': b (Proxy @Int) = ()
|
13 | b (Proxy @Int) = () -- This should compile, but doesn't
| ^^^^^^^^^^
--}
```
## Expected behavior
Accept and reject the same type applications in patterns as in expressions
## Environment
* GHC version used: 9.3.20210925
Optional:
* Operating System: Arch
* System Architecture: x86_649.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/20496Panic in pprMatch when "deriving Foldable" is used with -ddump-tc-trace2021-10-28T00:33:19ZArtyom KuznetsovPanic in pprMatch when "deriving Foldable" is used with -ddump-tc-trace## Summary
Trying to compile the following program in current HEAD with `-ddump-tc-trace` flag results in a panic:
```haskell
{-# LANGUAGE DeriveFoldable #-}
module Test where
data T a = MkT a
deriving Foldable
```
```
rndghc: panic...## Summary
Trying to compile the following program in current HEAD with `-ddump-tc-trace` flag results in a panic:
```haskell
{-# LANGUAGE DeriveFoldable #-}
module Test where
data T a = MkT a
deriving Foldable
```
```
rndghc: panic! (the 'impossible' happened)
GHC version 9.3.20211004:
pprMatch
CaseAlt
[f, (MkT a1)]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:181:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Hs/Expr.hs:1364:29 in ghc:GHC.Hs.Expr
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```
I know that this issue is already present in 6141aef49b, but I didn't check any further. 8.10.7 doesn't have this issue as far as I'm aware.
## Steps to reproduce
Run `ghc -ddump-tc-trace Test.hs` on the program above.
## Expected behavior
No panic :)
## Environment
* GHC version used: HEAD9.4.1Artyom KuznetsovArtyom Kuznetsovhttps://gitlab.haskell.org/ghc/ghc/-/issues/20527GHC 9.2 rejects certain poly-kinded unlifted newtype instances2022-02-13T02:59:37Zsheafsam.derbyshire@gmail.comGHC 9.2 rejects certain poly-kinded unlifted newtype instancesThe following program compiles on GHC 9.0, but on GHC 9.2 and HEAD it produces an error.
```haskell
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUA...The following program compiles on GHC 9.0, but on GHC 9.2 and HEAD it produces an error.
```haskell
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UnboxedTuples #-}
{-# LANGUAGE UnliftedNewtypes #-}
module NewtypeInstance where
import GHC.Exts
type DF :: TYPE r
data family DF
newtype instance DF = MkDF1 Int
newtype instance DF = MkDF2 Int#
newtype instance DF = MkDF3 (# Int#, Int, Word #)
newtype instance DF = MKDF4 (# (# #) | Float# #)
```
```
NewtypeInstance.hs:15:29: error:
* Expecting a lifted type, but `Int#' is unlifted
* In the type `Int#'
In the definition of data constructor `MkDF2'
In the newtype instance declaration for `DF'
|
15 | newtype instance DF = MkDF2 Int#
| ^^^^
NewtypeInstance.hs:16:29: error:
* Expecting a lifted type, but `(# Int#, Int, Word #)' is unlifted
* In the type `(# Int#, Int, Word #)'
In the definition of data constructor `MkDF3'
In the newtype instance declaration for `DF'
|
16 | newtype instance DF = MkDF3 (# Int#, Int, Word #)
| ^^^^^^^^^^^^^^^^^^^^^
NewtypeInstance.hs:17:29: error:
* Expecting a lifted type, but `(# (# #) | Float# #)' is unlifted
* In the type `(# (# #) | Float# #)'
In the definition of data constructor `MKDF4'
In the newtype instance declaration for `DF'
|
17 | newtype instance DF = MKDF4 (# (# #) | Float# #)
| ^^^^^^^^^^^^^^^^^^^^
```
I think the program should be accepted: we have an invisible kind argument which is taking a different value in each newtype instance. For some reason, starting with GHC 9.2, some defaulting seems to take place and we start expecting `r` to be `LiftedRep`.
I'm not sure what has caused the change in behaviour. Pinging the experts @rae and @RyanGlScott.9.2.1sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/20532Add a typing rule for dataToTag#2023-11-09T15:15:53ZKrzysztof GogolewskiAdd a typing rule for dataToTag#Because of parametricity, every polymorphic function `a -> Int#` should be constant (disregarding `_|_`).
However, `dataToTag# :: a -> Int#` breaks this: `dataToTag# False` is `0#`, `dataToTag# True` is `1#`.
I think `dataToTag#` shoul...Because of parametricity, every polymorphic function `a -> Int#` should be constant (disregarding `_|_`).
However, `dataToTag# :: a -> Int#` breaks this: `dataToTag# False` is `0#`, `dataToTag# True` is `1#`.
I think `dataToTag#` should have a special typing rule, just like `tagToEnum#`.
Possible ideas:
* The type should be a statically known algebraic data type. Currently `dataToTag#` returns `0#` for functions - I think that should be a type error. It can be used on newtypes - we can either continue allowing this, or reject and require `coerce`.
* Perhaps require that the constructors of the datatype are in scope
* Perhaps `dataToTag#` could be levity-polymorphic so that it works with UnliftedDatatypes
In `GHC.Base`, there's a wrapper `getTag x = dataToTag# x`. It can now be deprecated: it's no longer needed since ac977688523e5d.
Low priority: this function is rather obscure and mostly meant for `deriving`. This is probably best done after predicates #20000.https://gitlab.haskell.org/ghc/ghc/-/issues/20602Redundant-constraints warning complains about the wrong constraint2023-03-29T19:33:24ZRichard Eisenbergrae@richarde.devRedundant-constraints warning complains about the wrong constraintIf I say
```hs
{-# OPTIONS_GHC -Wredundant-constraints #-}
module Bug where
f :: (Eq a, Ord a) => a -> Bool
f x = x == x
```
GHC complains that the `Eq a` constraint is redundant... where it really should be the `Ord a` constraint th...If I say
```hs
{-# OPTIONS_GHC -Wredundant-constraints #-}
module Bug where
f :: (Eq a, Ord a) => a -> Bool
f x = x == x
```
GHC complains that the `Eq a` constraint is redundant... where it really should be the `Ord a` constraint that should be eliminated.
I will fix in ongoing work.9.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/20651ImpredicativeTypes vs. do notation2021-11-09T20:10:53ZDavid FeuerImpredicativeTypes vs. do notation## Summary
`do` notation doesn't work with `ImpredicativeTypes` even when its desugaring does.
## Steps to reproduce
```haskell
potato :: IO (forall a. a -> [a])
potato = readLn >>= \n -> pure (replicate n)
```
If I write
```haskell...## Summary
`do` notation doesn't work with `ImpredicativeTypes` even when its desugaring does.
## Steps to reproduce
```haskell
potato :: IO (forall a. a -> [a])
potato = readLn >>= \n -> pure (replicate n)
```
If I write
```haskell
potato >>= \f -> pure (f 3, f 'a')
```
it works fine.
If I instead write
```haskell
do
f <- potato
pure (f 3, f 'a')
```
I get
```
• Couldn't match type: forall a. a -> [a]
with: Char -> b
Expected: IO (Char -> b)
Actual: IO (forall a. a -> [a])
```
## Expected behavior
I expect `do` notation (without `ApplicativeDo`, etc.), to work (or not work) with impredicative types the same as its desugaring. I don't know enough about `ImpredicativeTypes` to know whether to expect both to succeed or both to fail, but the mismatch is jarring.
## Environment
* GHC version used: 9.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/20668decideMonoTyVars should take injectivity into account2022-02-23T13:21:43ZRichard Eisenbergrae@richarde.devdecideMonoTyVars should take injectivity into accountSuppose I have
```hs
{-# LANGUAGE TypeFamilies #-}
module Bug where
type family F a
inject :: a -> F a
inject = undefined
x = 5
f y = [inject y, x]
```
Important: the monomorphism restriction (MR) is in effect.
When inferring the ...Suppose I have
```hs
{-# LANGUAGE TypeFamilies #-}
module Bug where
type family F a
inject :: a -> F a
inject = undefined
x = 5
f y = [inject y, x]
```
Important: the monomorphism restriction (MR) is in effect.
When inferring the type of `f` at level 1, we have
```
x :: alpha[0]
[W] Num alpha[0]
y :: beta[1]
f :: beta[1] -> [alpha[0]]
[W] F beta[1] ~ alpha[0]
```
We now must decide what type to infer for `f`. GHC proceeds first by deciding the so-called mono tyvars (`decideMonoTyVars`). This works by taking all the type variables free in the environment (`alpha[0]`, in our case) and looking for any type variables used in an equality constraint with them. Because `beta[1]` is indeed in an equality constraint with `alpha[0]`, `beta[1]` is labeled as monomorphic, and thus is promoted to `beta[0]`. GHC then falls over because it won't default `alpha[0]` with the constraint `F beta[0] ~ alpha[0]` around, as that disrupts the rules for defaulting.
Instead, GHC should *not* label `beta[1]` as mono, because its appearance in the constraint is not an injective appearance.
I will fix in !5899.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/20675[regression] ghc 9.2.1 complains about "Uninferrable type variables" that ghc...2021-11-15T23:58:25ZJasonGross[regression] ghc 9.2.1 complains about "Uninferrable type variables" that ghc 9.0.1 can infer fine## Summary
Write a brief description of the issue.
## Steps to reproduce
Create a file `foo.hs` with the code
```haskell
{-# OPTIONS_GHC -cpp -XMagicHash #-}
{- For Hugs, use the option -F"cpp -P -traditional" -}
module Main where
i...## Summary
Write a brief description of the issue.
## Steps to reproduce
Create a file `foo.hs` with the code
```haskell
{-# OPTIONS_GHC -cpp -XMagicHash #-}
{- For Hugs, use the option -F"cpp -P -traditional" -}
module Main where
import qualified Prelude
#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base
#else
-- HUGS
import qualified IOExts
#endif
#ifdef __GLASGOW_HASKELL__
type Any = GHC.Base.Any
#else
-- HUGS
type Any = ()
#endif
data Type base_type =
Base base_type
| Arrow (Type base_type) (Type base_type)
type Interp base_type base_interp = Any
data Type0 base_type =
Type_base base_type
| Prod (Type0 base_type) (Type0 base_type)
| List (Type0 base_type)
| Option (Type0 base_type)
| Unit
type Interp0 base base_interp = Any
type ExprInfoT =
(Type (Type0 Any)) -> Any -> Interp (Type0 Any) (Interp0 Any Any)
-- singleton inductive, whose constructor was Build_ExprInfoT
type Base0 = Any
type Ident = Any
type Base_interp = Any
ident_interp :: ExprInfoT -> (Type (Type0 Base0)) -> Ident -> Interp (Type0 Base0) (Interp0 Base0 Base_interp)
ident_interp exprInfoT =
exprInfoT
seq :: a1 -> a2 -> a2
seq _ y =
y
main :: GHC.Base.IO ()
main =
seq ident_interp (GHC.Base.return ())
```
Run `ghc foo.hs -o foo` with ghc 9.0.1 (executed on GH Actions [here](https://github.com/JasonGross/test-haskell-bug/runs/4194435425?check_suite_focus=true)) and note that it completes fine. Run the same command with ghc 9.2.1 (executed on GH Actions [here](https://github.com/JasonGross/test-haskell-bug/runs/4194435468?check_suite_focus=true) and note that it errors with
```
foo.hs:37:1: error:
Error: • Uninferrable type variables k0, k1, k2 in
the type synonym right-hand side:
Type (Type0 (Any @{*}))
-> Any @{*}
-> Interp
@{*}
@{*}
@{k0}
(Type0 (Any @{*}))
(Interp0 @{k0} @{k1} @{k2} (Any @{k1}) (Any @{k2}))
• In the type declaration for ‘ExprInfoT’
|
37 | type ExprInfoT =
| ^^^^^^^^^^^^^^^^...
```
## Expected behavior
I expect code that compiles fine in 9.0.1 to continue compiling fine in 9.2.1. If this is not supposed to work, then Coq needs to be updated so that it can extract code compatible with Haskell 9.2.1 (see [coq/coq#15180](https://github.com/coq/coq/issues/15180))
## Environment
* GHC version used: 9.2.1 (failing), 9.0.1 (succeeding)
Optional:
* Operating System: Linux
* System Architecture:https://gitlab.haskell.org/ghc/ghc/-/issues/20873Using type-aliases in kind signatures requires DataKinds2022-09-05T05:37:27ZOleg GrenrusUsing type-aliases in kind signatures requires DataKinds```haskell
import qualified Data.Kind
type U = Data.Kind.Type
type MyMaybe :: U -> U
data MyMaybe a = MyJust a | MyNothing
```
fails with GHC-9.2.1 with
```
[1 of 1] Compiling Main ( ex.hs, interpreted )
ex.hs:5:17: erro...```haskell
import qualified Data.Kind
type U = Data.Kind.Type
type MyMaybe :: U -> U
data MyMaybe a = MyJust a | MyNothing
```
fails with GHC-9.2.1 with
```
[1 of 1] Compiling Main ( ex.hs, interpreted )
ex.hs:5:17: error:
• Type constructor ‘U’ cannot be used here
(perhaps you intended to use DataKinds)
• In a standalone kind signature for ‘MyMaybe’: U -> U
|
5 | type MyMaybe :: U -> U
| ^
Failed, no modules loaded.
```
This doesn't make sense to me?sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/20885Allow Well-Founded Recursion in Data Type Kinds2022-01-05T13:19:42ZAndrew MartinAllow Well-Founded Recursion in Data Type KindsGHC does not accept this program:
```
type Nat :: Type
data Nat = S Nat | Z
type Supertype :: Nat -> Type
data Supertype :: Nat -> Type where
SupertypeNext :: forall (n :: Nat) (super :: Supertype n). Ty n super -> Supertype ('S n)
...GHC does not accept this program:
```
type Nat :: Type
data Nat = S Nat | Z
type Supertype :: Nat -> Type
data Supertype :: Nat -> Type where
SupertypeNext :: forall (n :: Nat) (super :: Supertype n). Ty n super -> Supertype ('S n)
SupertypeDone :: Supertype 'Z
type Ty :: forall (n :: Nat) -> Supertype n -> Type
data Ty :: forall (n :: Nat) -> Supertype n -> Type where
Cons :: Ty ('S 'Z) ('SupertypeNext 'List)
Nil :: Ty ('S 'Z) ('SupertypeNext 'List)
List :: Ty 'Z 'SupertypeDone
```
GHC rejects the program with:
```
• Type constructor ‘Supertype’ cannot be used here
(it is defined and used in the same recursive group)
• In a standalone kind signature for ‘Ty’:
forall (n :: Nat) -> Supertype n -> Type
|
93 | type Ty :: forall (n :: Nat) -> Supertype n -> Type
| ^^^^^^^^^^^
```
Agda does accept its equivalent of this program:
```
data Nat : Set where
S : Nat -> Nat
Z : Nat
mutual
data Supertype : Nat -> Set where
SupertypeNext : (n : Nat) -> (super : Supertype n) -> Ty n super -> Supertype (S n)
SupertypeDone : Supertype Z
data Ty : (n : Nat) -> Supertype n -> Set where
List : Ty Z SupertypeDone
Cons : Ty (S Z) (SupertypeNext Z SupertypeDone List)
Nil : Ty (S Z) (SupertypeNext Z SupertypeDone List)
```
I am not sure if this is the same thing as induction recursion or not. That feature is discussed at #11962, but the example uses type families instead. The same issue may lie at the heart of both of these. Here, `Supertype`'s data constructors do not actually reference any of `Ty`'s data constructors, but `Ty`'s data constructors do reference `Supertype`'s data constructors.Research neededhttps://gitlab.haskell.org/ghc/ghc/-/issues/20894GHC 9.2 creates an unsafe coercion between a boxed and an unboxed type2022-02-09T16:26:28Zsheafsam.derbyshire@gmail.comGHC 9.2 creates an unsafe coercion between a boxed and an unboxed typeThe attached file (a single module with no dependencies, but unfortunately a bit long/complex) causes a Core Lint error on GHC 9.2. Compile with `-O1 -dcore-lint`.
GHC 9.0 and GHC HEAD both seem to not be affected.
```
warning:
...The attached file (a single module with no dependencies, but unfortunately a bit long/complex) causes a Core Lint error on GHC 9.2. Compile with `-O1 -dcore-lint`.
GHC 9.0 and GHC HEAD both seem to not be affected.
```
warning:
Unsafe coercion: between unboxed and boxed value
From: ()
To: Int#
```
[Bug.hs](/uploads/45e865bdbcd94302b9f6fcd45bd93005/Bug.hs)
In the `dump-ds-preopt` output I am seeing some worrying coercions, e.g.
```haskell
$d~_a1c4 :: MyInt ~ 'LitTy
[LclId]
$d~_a1c4
= GHC.Types.Eq#
@(Type 'KEmpty 'Type)
@MyInt
@'LitTy
@~(<'LitTy>_N :: 'LitTy GHC.Prim.~# 'LitTy)
```
but here the promoted `LitTy` constructor is insufficiently applied. It seems that the definition of the promoted data constructor `LitTy` confuses GHC, as it only takes invisible arguments.
I haven't investigated further or identified which commits broke or fixed this yet. @rae?9.2.2https://gitlab.haskell.org/ghc/ghc/-/issues/20916GHC accepts two names for the same kind variable2022-03-22T09:32:12ZSimon Peyton JonesGHC accepts two names for the same kind variableConsider
```
{-# LANGUAGE CUSKs, EmptyDataDecls, PolyKinds, KindSignatures #-}
data SameKind (a :: k) (b :: k)
data T1 (a :: p) (b :: q) c = MkT (SameKind a b) c
```
GHC rejects this with
```
Foo.hs:10:9: error:
• Different names fo...Consider
```
{-# LANGUAGE CUSKs, EmptyDataDecls, PolyKinds, KindSignatures #-}
data SameKind (a :: k) (b :: k)
data T1 (a :: p) (b :: q) c = MkT (SameKind a b) c
```
GHC rejects this with
```
Foo.hs:10:9: error:
• Different names for the same type variable: ‘p’ and ‘q’
• In the data declaration for ‘T’
|
10 | data T1 (a :: p) (b :: q) c = MkT (SameKind a b) c
| ^^^^^^^^^^^^^^^^^^
```
If T is a CUSK, it is similarly rejected, abeit with a different message
```
{-# LANGUAGE CUSKs, EmptyDataDecls, PolyKinds, KindSignatures #-}
data SameKind (a :: k) (b :: k)
data T2 (a :: p) (b :: q) = MkT (SameKind a b)
```
we get
```
Foo.hs:10:45: error:
• Expected kind ‘p’, but ‘b’ has kind ‘q’
‘q’ is a rigid type variable bound by
the data type declaration for ‘T2’
at Foo.hs:10:10-24
‘p’ is a rigid type variable bound by
the data type declaration for ‘T2’
at Foo.hs:10:10-24
• In the second argument of ‘SameKind’, namely ‘b’
In the type ‘(SameKind a b)’
In the definition of data constructor ‘MkT’
|
10 | data T2 (a :: p) (b :: q) = MkT (SameKind a b)
| ^
```
because `p` and `q` are created as distinct skolems.
BUT alas with standalone kind signatures we don't this
```
{-# LANGUAGE CUSKs, EmptyDataDecls, PolyKinds, KindSignatures, StandaloneKindSignatures #-}
type T3 :: k -> k -> Type
data T3 (a :: p) (b :: q) = MkT
```
This is accepted by HEAD. That's highly inconsistent. We should reject.Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/20921Regression in ambiguity checking for partial type signatures in GHC 9.22022-02-21T11:13:10Zsheafsam.derbyshire@gmail.comRegression in ambiguity checking for partial type signatures in GHC 9.2The following program compiles on all GHC versions ranging from `8.6` to `9.0`, but fails on `9.2` and HEAD:
```haskell
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE ...The following program compiles on all GHC versions ranging from `8.6` to `9.0`, but fails on `9.2` and HEAD:
```haskell
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module PsigBug where
import Data.Kind
( Constraint )
import GHC.TypeLits
( ErrorMessage(..), TypeError )
import GHC.TypeNats ( Nat )
type family OK (i :: Nat) :: Constraint where
OK 1 = ()
OK 2 = ()
OK n = TypeError (ShowType n :<>: Text "is not OK")
class C (i :: Nat) where
foo :: Int
instance C 1 where
foo = 1
instance C 2 where
foo = 2
type family Boo (i :: Nat) :: Nat where
Boo i = i
bar :: Int
bar =
let
quux :: forall (i :: Nat). ( OK (Boo i), _ ) => Int
quux = foo @(Boo i)
in quux @1 + quux @2
```
```
PsigBug.hs:38:5: error:
* Could not deduce: OK i0
from the context: (OK (Boo i), C i)
bound by the inferred type for `quux':
forall (i :: Nat). (OK (Boo i), C i) => Int
at PsigBug.hs:38:5-23
* When checking that the inferred type
quux :: forall {i :: Nat}. (OK (Boo i), OK i, C i) => Int
is as general as its (partial) signature
quux :: forall (i :: Nat). (OK (Boo i), C i) => Int
In the expression:
let
quux :: forall (i :: Nat). (OK (Boo i), _) => Int
quux = foo @(Boo i)
in quux @1 + quux @2
In an equation for `bar':
bar
= let
quux :: forall (i :: Nat). (OK (Boo i), _) => Int
quux = foo @(Boo i)
in quux @1 + quux @2
|
38 | quux = foo @(Boo i)
| ^^^^^^^^^^^^^^^^^^^
PsigBug.hs:38:5: error:
* Could not deduce (C i0)
from the context: (OK (Boo i), C i)
bound by the inferred type for `quux':
forall (i :: Nat). (OK (Boo i), C i) => Int
at PsigBug.hs:38:5-23
The type variable `i0' is ambiguous
* When checking that the inferred type
quux :: forall {i :: Nat}. (OK (Boo i), OK i, C i) => Int
is as general as its (partial) signature
quux :: forall (i :: Nat). (OK (Boo i), C i) => Int
In the expression:
let
quux :: forall (i :: Nat). (OK (Boo i), _) => Int
quux = foo @(Boo i)
in quux @1 + quux @2
In an equation for `bar':
bar
= let
quux :: forall (i :: Nat). (OK (Boo i), _) => Int
quux = foo @(Boo i)
in quux @1 + quux @2
|
38 | quux = foo @(Boo i)
| ^^^^^^^^^^^^^^^^^^^
```
These messages mention an ambiguous variable `i0`... but it doesn't actually appear anywhere in the rest of the messages!
This bug prevents one of my libraries from compiling (and I couldn't find a workaround), so this is not only of theoretical interest.9.2.2Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/20922Constructors applied to type variables behave differently starting on GHC 9.22022-02-23T13:21:43Zsheafsam.derbyshire@gmail.comConstructors applied to type variables behave differently starting on GHC 9.2The following program compiles on GHC 8.6 to 9.0 but fails to compile on GHC 9.2 and HEAD. (Apologies for not reducing the test case further.)
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-...The following program compiles on GHC 8.6 to 9.0 but fails to compile on GHC 9.2 and HEAD. (Apologies for not reducing the test case further.)
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module PatternsBug where
import Data.Kind
( Type )
import Data.Proxy
( Proxy(..) )
import Data.Type.Equality
( (:~:)(Refl) )
import Unsafe.Coerce
( unsafeCoerce )
passGetterIndex
:: forall (js :: [Type]) (jss :: [[Type]]) (s :: Type) (as :: [Type])
. SSameLength js as -> HList js -> Viewers (js ': jss) s as -> Viewers jss s as
passGetterIndex (SSameSucc ( same1 :: SSameLength t_js t_as ) ) js views =
case ( js, views ) of
( (k :: j) :> (ks :: HList t_js), ConsViewer same2 (_ :: Proxy is) (_ :: Proxy iss) _ getters ) ->
case same2 of
( sameSucc@(SSameSucc (same3 :: SSameLength t_is jss) ) ) ->
case sameSucc of
( _ :: SSameLength (i ': t_is) (js ': jss) )
| Refl <- ( unsafeCoerce Refl :: ZipCons t_is (Tail iss) :~: jss )
, Refl <- ( unsafeCoerce Refl :: ( t_js ': MapTail jss ) :~: iss )
, Refl <- ( unsafeCoerce Refl :: i :~: j )
-- , Proxy :: Proxy bss <- Proxy @(Tail iss)
-> ConsViewer same3 (Proxy @t_is) (Proxy @(Tail iss)) Proxy
( passGetterIndex @t_js @(MapTail jss) @s @t_as same1 ks getters )
data Viewers (iss :: [[Type]]) (s :: Type) (as :: [Type]) where
-- NilViewer ...
ConsViewer :: forall (is :: [Type]) (s :: Type) (a :: Type) (iss :: [[Type]]) (as :: [Type])
. SSameLength is (ZipCons is iss)
-> Proxy is
-> Proxy iss
-> Proxy a
-> Viewers iss s as
-> Viewers (ZipCons is iss) s (a ': as)
data SSameLength (is :: [k]) (js :: [l]) where
SSameZero :: SSameLength '[] '[]
SSameSucc :: SSameLength is js -> SSameLength (i ': is) (j ': js)
infixr 3 :>
data HList (as :: [Type]) where
HNil :: HList '[]
(:>) :: a -> HList as -> HList (a ': as)
type family ListVariadic (as :: [Type]) (b :: Type) = (r :: Type) | r -> as b where
type family ZipCons (as :: [k]) (bss :: [[k]]) = (r :: [[k]]) | r -> as bss where
ZipCons '[] '[] = '[]
ZipCons (a ': as) (bs ': bss) = (a ': bs) ': ZipCons as bss
type family Tail (x :: [k]) :: [k] where
Tail (_ ': xs) = xs
type family MapTail (x :: [[k]]) :: [[k]] where
MapTail '[] = '[]
MapTail (xs ': xss) = Tail xs ': MapTail xss
```
The problem lies in the `Proxy @(Tail iss)` argument to the constructor `ConsViewer`. It causes the following error starting on GHC 9.2:
```
PatternsBug.hs:35:18: error:
* Could not deduce: ZipCons is2 bss ~ jss
from the context: (js ~ (i : is), as ~ (j : js1))
bound by a pattern with constructor:
SSameSucc :: forall {k} {l} (is :: [k]) (js :: [l]) (i :: k)
(j :: l).
SSameLength is js -> SSameLength (i : is) (j : js),
in an equation for `passGetterIndex'
at PatternsBug.hs:24:18-61
or from: ((js : jss) ~ ZipCons is1 iss, as ~ (a1 : as2))
bound by a pattern with constructor:
ConsViewer :: forall (is :: [*]) s a (iss :: [[*]]) (as :: [*]).
SSameLength is (ZipCons is iss)
-> Proxy is
-> Proxy iss
-> Proxy a
-> Viewers iss s as
-> Viewers (ZipCons is iss) s (a : as),
in a case alternative
at PatternsBug.hs:26:39-97
or from: (is1 ~ (i1 : is2), ZipCons is1 iss ~ (j1 : js2))
bound by a pattern with constructor:
SSameSucc :: forall {k} {l} (is :: [k]) (js :: [l]) (i :: k)
(j :: l).
SSameLength is js -> SSameLength (i : is) (j : js),
in a case alternative
at PatternsBug.hs:28:21-61
or from: jss ~ ZipCons is2 (Tail iss)
bound by a pattern with constructor:
Refl :: forall {k} (a :: k). a :~: a,
in a pattern binding in
a pattern guard for
a case alternative
at PatternsBug.hs:31:17-20
or from: iss ~ (is : MapTail jss)
bound by a pattern with constructor:
Refl :: forall {k} (a :: k). a :~: a,
in a pattern binding in
a pattern guard for
a case alternative
at PatternsBug.hs:32:17-20
Expected: Viewers jss s as
Actual: Viewers (ZipCons is2 bss) s (j : js1)
`jss' is a rigid type variable bound by
the type signature for:
passGetterIndex :: forall (js :: [*]) (jss :: [[*]]) s (as :: [*]).
SSameLength js as
-> HList js -> Viewers (js : jss) s as -> Viewers jss s as
at PatternsBug.hs:(21,1)-(23,81)
* In the expression:
ConsViewer
same3 (Proxy @t_is) (Proxy @(Tail iss)) Proxy
(passGetterIndex @t_js @(MapTail jss) @s @t_as same1 ks getters)
In a case alternative:
(_ :: SSameLength (i : t_is) (js : jss))
| Refl <- (unsafeCoerce Refl :: ZipCons t_is (Tail iss) :~: jss),
Refl <- (unsafeCoerce Refl :: (t_js : MapTail jss) :~: iss),
Refl <- (unsafeCoerce Refl :: i :~: j)
-> ConsViewer
same3 (Proxy @t_is) (Proxy @(Tail iss)) Proxy
(passGetterIndex @t_js @(MapTail jss) @s @t_as same1 ks getters)
In the expression:
case sameSucc of
(_ :: SSameLength (i : t_is) (js : jss))
| Refl <- (unsafeCoerce Refl :: ZipCons t_is (Tail iss) :~: jss),
Refl <- (unsafeCoerce Refl :: (t_js : MapTail jss) :~: iss),
Refl <- (unsafeCoerce Refl :: i :~: j)
-> ConsViewer
same3 (Proxy @t_is) (Proxy @(Tail iss)) Proxy
(passGetterIndex @t_js @(MapTail jss) @s @t_as same1 ks getters)
* Relevant bindings include
same3 :: SSameLength is2 jss (bound at PatternsBug.hs:28:32)
views :: Viewers (js : jss) s as (bound at PatternsBug.hs:24:68)
passGetterIndex :: SSameLength js as
-> HList js -> Viewers (js : jss) s as -> Viewers jss s as
(bound at PatternsBug.hs:24:1)
|
35 | -> ConsViewer same3 (Proxy @t_is) (Proxy @(Tail iss)) Proxy
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
PatternsBug.hs:35:50: error:
* Couldn't match type `bss' with `MapTail jss'
Expected: Proxy bss
Actual: Proxy (Tail iss)
`bss' is untouchable
inside the constraints: a ~ i1
bound by a pattern with constructor:
Refl :: forall {k} (a :: k). a :~: a,
in a pattern binding in
a pattern guard for
a case alternative
at PatternsBug.hs:33:17-20
* In the third argument of `ConsViewer', namely
`(Proxy @(Tail iss))'
In the expression:
ConsViewer
same3 (Proxy @t_is) (Proxy @(Tail iss)) Proxy
(passGetterIndex @t_js @(MapTail jss) @s @t_as same1 ks getters)
In a case alternative:
(_ :: SSameLength (i : t_is) (js : jss))
| Refl <- (unsafeCoerce Refl :: ZipCons t_is (Tail iss) :~: jss),
Refl <- (unsafeCoerce Refl :: (t_js : MapTail jss) :~: iss),
Refl <- (unsafeCoerce Refl :: i :~: j)
-> ConsViewer
same3 (Proxy @t_is) (Proxy @(Tail iss)) Proxy
(passGetterIndex @t_js @(MapTail jss) @s @t_as same1 ks getters)
* Relevant bindings include
same3 :: SSameLength is2 jss (bound at PatternsBug.hs:28:32)
views :: Viewers (js : jss) s as (bound at PatternsBug.hs:24:68)
passGetterIndex :: SSameLength js as
-> HList js -> Viewers (js : jss) s as -> Viewers jss s as
(bound at PatternsBug.hs:24:1)
|
35 | -> ConsViewer same3 (Proxy @t_is) (Proxy @(Tail iss)) Proxy
| ^^^^^^^^^^^^^^^^^
```
Rather curiously, if you uncomment the line
```haskell
Proxy :: Proxy bss <- Proxy @(Tail iss)
```
and use `bss` instead of `Tail iss` just below, writing:
```haskell
-> ConsViewer same3 (Proxy @t_is) (Proxy @bss) Proxy
( passGetterIndex @t_js @(MapTail jss) @s @t_as same1 ks getters )
```
then all of a sudden GHC 9.2 accepts this program again. So it seems like there is a special treament for type variables compared to other types. This perhaps makes when the constructor is used as a pattern, but it's rather strange that it would make any difference when it's an expression.9.2.2Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/20929Different error with representation-polymorphic binder2022-02-03T00:53:58ZKrzysztof GogolewskiDifferent error with representation-polymorphic binderThis program is correctly rejected:
```haskell
{-# LANGUAGE TypeFamilies #-}
module M where
import GHC.Types
type family Q :: k
type family F :: forall (r :: RuntimeRep) -> TYPE r
f :: Bool
f = let a :: F Q; a = undefined in True
```...This program is correctly rejected:
```haskell
{-# LANGUAGE TypeFamilies #-}
module M where
import GHC.Types
type family Q :: k
type family F :: forall (r :: RuntimeRep) -> TYPE r
f :: Bool
f = let a :: F Q; a = undefined in True
```
```
• The binder ‘a’ does not have a fixed runtime representation:
F Q :: TYPE Q
```
However, if I change the last line to
```haskell
f = let a :: F r; a = undefined in True
```
I get a different, worse error message:
```
• Expected a type, but ‘F r’ has kind ‘TYPE r’
‘r’ is a rigid type variable bound by
the type signature for ‘a’
at M.hs:10:9-16
```
I'd expect to get the same error in both cases, mentioning no having fixed representation. I suspect there's an extraneous test that is now redundant with the new fixed representation checks.
As far as I can tell, this is not caused by the bug #20837 in `isLiftedType_maybe` - cherry-picking 56e041bb7ac254eaa500317c75731a862cd1ec82 does not solve it.https://gitlab.haskell.org/ghc/ghc/-/issues/20932Inconsistent tidying of implications2022-02-06T02:53:52ZSimon Peyton JonesInconsistent tidying of implicationsConsider this program (`tcfail013`)
```
f [] = 1
f True = 2
```
We get the unsolved implication
```
Wanted: WC {wc_impl =
Implic {
TcLevel = 1
Skolems = a_aur[sk:1] a_axQ[sk:1]
...Consider this program (`tcfail013`)
```
f [] = 1
f True = 2
```
We get the unsolved implication
```
Wanted: WC {wc_impl =
Implic {
TcLevel = 1
Skolems = a_aur[sk:1] a_axQ[sk:1]
Given-eqs = NoGivenEqs
Status = Insoluble
Given =
Wanted =
WC {wc_simple =
[WD] hole{co_axS} {0}:: Bool ~# [a_aur[sk:1]] (CIrredCan(shape))
[WD] $dNum_axR {0}:: Num a_axQ[sk:1] (CDictCan(psc))}
Binds = EvBindsVar<axY>
the inferred type of f :: [a_aur[sk:1]] -> a_axQ[sk:1] }}
```
Note that the two skolems have the same `OccName`, namely `a`. (They both started life as
unification variablex, which we generalised.)
When we tidy the skolems we get
```
reportImplic
Implic {
TcLevel = 1
Skolems = a_auG[sk:1] a1_ay2[sk:1]
Given-eqs = NoGivenEqs
Status = Insoluble
Given =
Wanted =
WC {wc_simple =
[WD] hole{co_ay4} {0}:: Bool
GHC.Prim.~# [a_auG[sk:1]] (CIrredCan(shape))
[WD] $dNum_ay3 {0}:: Num a_ay2[sk:1] (CDictCan(psc))}
Binds = EvBindsVar<ay9>
the inferred type of f :: [a_auG[sk:1]] -> a1_ay2[sk:1] }
```
We have tidied one `a` to `a`, and the other to `a1`. This flat-out contradicts
`Note [Tidying multiple names at once]` in `GHC.Types.Names.Occurrence` in GHC.Types.Names.Occurrence,
where we say that we should not accidentally privilege one of these 'a's over the others.
The reason we don't follow the standard guidance is that in `reportImplic` we have
```
(env1, tvs') = mapAccumL tidyVarBndr (cec_tidy ctxt) $
scopedSort tvs
```
If instead we had
```
(env1, tvs') = tidyVarBndrs (cec_tidy ctxt) $
scopedSort tvs
```
then `tidyVarBndrs` would do the symmetric thing. In our example we'd tidy to `a1` and `a2`.
I think we should do the symmetric thing. But we get a couple of dozen regression failures, as
error messages wibble around. Task: make the change, check the changes, and accept them.
The status quo seems wrong to me.Matthew PickeringMatthew Pickeringhttps://gitlab.haskell.org/ghc/ghc/-/issues/20933matchInstEnv accounts for 50% of typechecker time2022-02-09T17:33:58ZMatthew PickeringmatchInstEnv accounts for 50% of typechecker time![2022-01-11-120537_1838x781](/uploads/54981218c0deaf225d86e747e120fcbf/2022-01-11-120537_1838x781.png)
I created a profile of GHC compiling a large commercial project and noticed that `matchInstEnv` accounted for 50% of time spent type...![2022-01-11-120537_1838x781](/uploads/54981218c0deaf225d86e747e120fcbf/2022-01-11-120537_1838x781.png)
I created a profile of GHC compiling a large commercial project and noticed that `matchInstEnv` accounted for 50% of time spent typechecking the project. That seems like rather a lot. Zooming into just `matchInstEnv`..
![2022-01-11-120754_1917x288](/uploads/caa8b8a41042b4725d2a3685652b00ad/2022-01-11-120754_1917x288.png)
It seems that the cost is split quite evenly between `tc_unify_tys_fg`, `tc_match_tys` and `$instIsVisible`, `instIsVisible` looks quite cheap so I wondered if this function is getting hammered an ungodly number of times.https://gitlab.haskell.org/ghc/ghc/-/issues/20972Use ConcreteTv for metavariables that must only be unified with concrete types2022-04-14T20:54:50Zsheafsam.derbyshire@gmail.comUse ConcreteTv for metavariables that must only be unified with concrete typesCurrently, when we have a constraint of the form `Concrete# ty`, we have a separate evidence term in the form of a coercion hole `{co} :: ty #~ concrete_tv`, for some metavariable `concrete_tv`. This metavariable really belongs to this `...Currently, when we have a constraint of the form `Concrete# ty`, we have a separate evidence term in the form of a coercion hole `{co} :: ty #~ concrete_tv`, for some metavariable `concrete_tv`. This metavariable really belongs to this `Concrete#` constraint, and should not be unified with anything else. This isn't a problem in PHASE 1 of the FixedRuntimeRep plan outlined [on the wiki](https://gitlab.haskell.org/ghc/ghc/-/wikis/FixedRuntimeRep), because the metavariable `concrete_tv` never leaks out. However, once we start actually using the evidence for these constraints, we will insert casts into the typechecked program and suddenly it becomes possible for some other part of the typechecker to unify this metavariable. If we end up unifying with a non-concrete type (e.g. a type family application), then the whole exercise will have been for nought.
The plan to address this is to introduce a special kind of metavariable that can only be unified with concrete types, by adding a new field to `MetaInfo`, say `ConcreteTv`.
## Using ConcreteTv instead of Concrete# constraints
@simonpj then points out that, once we do this, then perhaps we no longer need the `Concrete#` special predicate at all, and could instead work directly with `ConcreteTv` metavariables. I've started thinking about this, here are a few observations:
### Phase 2 for free?
Using `ConcreteTv` directly allows us to re-use GHC's existing infrastructure for inserting casts in some circumstances, instead of manually having to insert them as described in the [FixedRuntimeRep wiki page](https://gitlab.haskell.org/ghc/ghc/-/wikis/FixedRuntimeRep#phase-2).
For example:
```haskell
f x = ... g x ...
g :: forall (a :: TYPE (F Int)). a -> ...
type family F a where
F Int = LiftedRep
```
When typechecking `f`, if we can set things up to have `x :: ty :: TYPE conc_tv` for `conc_tv` one of these `ConcreteTv` metavariables, then we've in very good shape. Indeed, then we will refuse to unify `conc_tv := F Int` because `F Int` is not concrete, but we will rewrite `conc_tv ~# F_Int` to `conc_tv ~# LiftedRep` and will unify `conc_tv := LiftedRep`. Then the rest of the machinery in `tcApp` will insert the necessary casts for the application `g x`.
The problem, as far as I see it, is that this optimistically assumes that the relevant metavariables are assigned `ConcreteTv` at birth. In this particular case I think we're OK: the first thing we see is `x` in a binding position but we otherwise know nothing about `x`, so it stands to reason that we can conjure up a `ConcreteTv` metavariable for its kind and go from there.
However, now that I look at where the existing `hasFixedRuntimeRep` checks take place, we might well instead come across a type first (and do some unification), and only later come across a situation which requires concreteness (e.g. it appears as the kind of a bound variable).
It seems plausible to me that we could end up in a situation where we have `x :: ty :: alpha` for a normal unification variable `alpha`, then we unify `alpha ~ F Int`, and then later on we come across e.g. `x` used in an application, realising too late "oh shoot, we should have made `alpha` a `ConcreteTv`!".
### Error messages
Currently, metavariables don't store any origin information. If we want to report informative representation-polymorphism error messages, we should add some origin information so that if we end up with an unfilled `ConcreteTv` metavariable we can report an appropriate error message.
### Re-using `~#`
It seems like we might benefit from re-using primitive equality. In particular, decomposition of `Concrete#` constraints is quite similar to decomposition for `~#`, so it seems to make sense.
When we come across a type `ty` that we must ensure is concrete, we create a new `ConcreteTv` metavariable `conc_tv` and directly emit `ty ~# conc_tv`. We can attach a `CtOrigin` just as before, so we still have the error messages.
This would avoid a fair bit of special casing, as currently `Concrete#` is unique in the fact that the predicate `Concrete# a` does not match the type of its evidence `a ~ concrete_tv`.sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/20974GHCi >= 9.2.1 prints type signatures containing type families in an ugly way2022-05-20T08:22:33ZAndrzej RybczakGHCi >= 9.2.1 prints type signatures containing type families in an ugly wayConsider the following:
```haskell
{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, TypeOperators #-}
import Data.Kind
class A (m :: Type -> Type)
class B (m :: Type -> Type)
type family F cs (m :: Type -> Type) :: Constraint wh...Consider the following:
```haskell
{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, TypeOperators #-}
import Data.Kind
class A (m :: Type -> Type)
class B (m :: Type -> Type)
type family F cs (m :: Type -> Type) :: Constraint where
F '[] m = ()
F (c : cs) m = (c m, F cs m)
test :: F [Monad, A, B] m => m ()
test = pure ()
```
The type signature of `test` is pretty-printed in GHCi 9.0.2 and lower:
```
$ ghci-9.0.2
GHCi, version 9.0.2: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/unknown/.ghci
>>> :l test
[1 of 1] Compiling Main ( test.hs, interpreted )
Ok, one module loaded.
>>> :t test
test :: (Monad m, A m, B m) => m ()
```
but this is what happens in 9.2.1 and HEAD:
```
$ ghci-9.2.1
GHCi, version 9.2.1: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/unknown/.ghci
>>> :l test.hs
[1 of 1] Compiling Main ( test.hs, interpreted )
Ok, one module loaded.
>>> :t test
test :: (Monad m, (A m, (B m, () :: Constraint))) => m ()
```
Looks much worse and I'd consider that a regression.9.2.2sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/21006Unhelpful Kind equality error at the start of file2022-01-28T10:50:09ZJkensikUnhelpful Kind equality error at the start of fileI get an error
```
app\Main.hs:1:1: error:
Couldn't match kind `*' with `Constraint'
When matching types
b :: *
(Set b, Set s) :: Constraint
|
1 | {-# LANGUAGE TypeFamilies #-}
| ^
```
I don't know why b and the ...I get an error
```
app\Main.hs:1:1: error:
Couldn't match kind `*' with `Constraint'
When matching types
b :: *
(Set b, Set s) :: Constraint
|
1 | {-# LANGUAGE TypeFamilies #-}
| ^
```
I don't know why b and the constraint (Set b, Set s) are being matched? I would expect the constraint to existentially quantify the type b but why would it be matching them?
I believe the last thing I changed before getting the error was adding OpOutcome to the class.
here is the code
```
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE RankNTypes #-}
module Main where
import GHC.TypeLits (Symbol)
import GHC.Exts (Constraint)
import Data.Reflection (Reifies, reflect)
import Data.Proxy (Proxy(..))
main :: IO ()
main = print 5
class ((a,b)::Constraint) => HasCtxt a b
instance (a,b) => HasCtxt a b
class Determines a b | a -> b
instance Determines a b => Determines a b
type Set b = (b ~ b)
type OpLayout a = (forall s ctxt b. (OpCtxt a s b ~ ctxt, Determines a b, Determines a ctxt,Reifies s b) => ( HasCtxt ctxt (Reifies s b))) :: Constraint
data Stack a where
Cons :: OpConstructor a -> Stack b -> Stack a
Nil :: Stack "NIL"
class OpLayout a => OpCode (a::Symbol) where
type OpCtxt a s b = (ctxt :: Constraint) | ctxt -> s b
type OpOutcome a :: *
data OpConstructor a
opValue :: Determines a s => Proxy s
opValue = Proxy
popOP :: OpCtxt a s b => Stack a -> (b :: *)
evalOP :: OpConstructor a -> Stack x -> OpOutcome a
instance OpCode "load_val" where
type OpCtxt "load_val" s b = (Set s, Set b)
type OpOutcome "load_val" = Stack "load_val"
data OpConstructor "load_val" = forall b. LOAD_VAL b
popOP stack = reflect opValue
evalOP op stack = op `Cons` stack
```https://gitlab.haskell.org/ghc/ghc/-/issues/21010ASSERTION failure when building subcategories2022-02-08T11:01:59ZMatthew PickeringASSERTION failure when building subcategories```
[ 5 of 13] Compiling Control.Subcategory.Bind ( src/Control/Subcategory/Bind.hs, dist/build/Control/Subcategory/Bind.o, dist/build/Control/Subcategory/Bind.dyn_o )
<no location info>: error:
ASSERT failed!
CallStack (from HasC...```
[ 5 of 13] Compiling Control.Subcategory.Bind ( src/Control/Subcategory/Bind.hs, dist/build/Control/Subcategory/Bind.o, dist/build/Control/Subcategory/Bind.dyn_o )
<no location info>: error:
ASSERT failed!
CallStack (from HasCallStack):
massert, called at compiler/GHC/Tc/Solver/Canonical.hs:2485:10 in ghc:GHC.Tc.Solver.Canonical
```
Which is this assertion in `GHC.Tc.Solver.Canonical.canEqCanLHSFinish`.
```
-- by now, (TyEq:N) is already satisfied (if applicable)
; massert (not bad_newtype)
```
Standalone repro: https://gist.github.com/540cf5453a26825e6885ad59cb01957a
Run using `./run`
```
[nix-shell:~/subcategories-0.1.1.0/repro]$ ./run
[1 of 4] Compiling MonoTraversable ( MonoTraversable.hs, out/MonoTraversable.o, out/MonoTraversable.dyn_o )
[2 of 4] Compiling Internal ( Internal.hs, out/Internal.o, out/Internal.dyn_o )
[3 of 4] Compiling BindA ( BindA.hs, out/BindA.o, out/BindA.dyn_o )
[4 of 4] Compiling Bind ( Bind.hs, out/Bind.o, out/Bind.dyn_o )
<no location info>: error:
ASSERT failed!
CallStack (from HasCallStack):
massert, called at compiler/GHC/Tc/Solver/Canonical.hs:2485:10 in ghc:GHC.Tc.Solver.Canonical
```https://gitlab.haskell.org/ghc/ghc/-/issues/21023MonoLocalBinds sometimes monomorphises *global* binds2022-03-07T22:09:56ZRichard Eisenbergrae@richarde.devMonoLocalBinds sometimes monomorphises *global* bindsHere is a fairly simple program:
```hs
{-# LANGUAGE MonoLocalBinds #-}
module Bug where
x = 5
f y = (x, y)
```
Important: the monomorphism restriction is in effect.
GHC embarrassingly infers the type `Any -> (Integer, Any)` for `f`...Here is a fairly simple program:
```hs
{-# LANGUAGE MonoLocalBinds #-}
module Bug where
x = 5
f y = (x, y)
```
Important: the monomorphism restriction is in effect.
GHC embarrassingly infers the type `Any -> (Integer, Any)` for `f`. This is because `f`'s right-hand side mentions `x`, whose type is not yet known. (The monomorphism restriction means it's type is not `Num a => a`.) So, GHC chooses the `NoGen` plan for generalization. With nothing to say what the type of `y` should be, GHC picks `Any`. Bad GHC, bad. Giving `x` a type signature or disabling the monomorphism restriction fixes the problem.
I think the solution is simply never to do `NoGen` for top-level bindings.Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/21038GHC 9.2.1 typechecking regression with RankNTypes and TemplateHaskell2022-02-14T13:59:23ZRyan ScottGHC 9.2.1 typechecking regression with RankNTypes and TemplateHaskellWhile porting some code over to use GHC 9.2.1, I noticed a typechecking regression that doesn't appear to be explained in the 9.2.1 release notes. Here is a minimal example:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell...While porting some code over to use GHC 9.2.1, I noticed a typechecking regression that doesn't appear to be explained in the 9.2.1 release notes. Here is a minimal example:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
module Bug where
data Foo = MkFoo (forall a. a -> a)
worksOnAllGHCs1 :: Foo
worksOnAllGHCs1 = MkFoo (\x -> x)
worksOnAllGHCs2 :: Foo
worksOnAllGHCs2 = MkFoo $ \x -> x
worksOnAllGHCs3 :: Foo
worksOnAllGHCs3 = $([| MkFoo |]) (\x -> x)
doesn'tWorkOnGHC9'2 :: Foo
doesn'tWorkOnGHC9'2 = $([| MkFoo |]) $ \x -> x
```
All four of these top-level functions will typecheck on GHC 9.0.2 and earlier. On GHC 9.2.1 and HEAD, `worksOnAllGHCs{1,2,3}` functions will typecheck, but the `doesn'tWorkOnGHC9'2` function will not typecheck:
```
$ ghc-9.2.1 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o, Bug.dyn_o )
Bug.hs:17:24: error:
• Couldn't match type: forall a. a -> a
with: p0 -> p0
Expected: (p0 -> p0) -> Foo
Actual: (forall a. a -> a) -> Foo
• In the first argument of ‘($)’, namely ‘(MkFoo)’
In the expression: (MkFoo) $ \ x -> x
In an equation for ‘doesn'tWorkOnGHC9'2’:
doesn'tWorkOnGHC9'2 = (MkFoo) $ \ x -> x
|
17 | doesn'tWorkOnGHC9'2 = $([| MkFoo |]) $ \x -> x
| ^^^^^^^^^^^^^
```
I'm unclear why using a Template Haskell splice would affect typechecking like this, so I believe this is a bug.9.2.2Ryan ScottRyan Scotthttps://gitlab.haskell.org/ghc/ghc/-/issues/21040Curious kind-checking failure with GHC 9.2.1 and visible dependent quantifica...2022-02-04T14:33:59ZRyan ScottCurious kind-checking failure with GHC 9.2.1 and visible dependent quantificationWhile porting some code over to GHC 9.2.1 recently, I noticed an unusual quirk in the way kind inference interacts with visible dependent quantification. Consider these two modules:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTyp...While porting some code over to GHC 9.2.1 recently, I noticed an unusual quirk in the way kind inference interacts with visible dependent quantification. Consider these two modules:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
module A where
import Data.Kind
type T1 :: Type -> Type
data T1 a = MkT1
t1FunA :: (forall a. T1 a -> r) -> r
t1FunA g = g MkT1
t1FunB :: T1 a -> T1 a -> ()
t1FunB _ _ = ()
type T2 :: forall (a :: Type) -> Type
data T2 a = MkT2
t2FunA :: (forall a. T2 a -> r) -> r
t2FunA g = g MkT2
t2FunB :: T2 a -> T2 a -> ()
t2FunB _ _ = ()
```
```hs
{-# LANGUAGE NoPolyKinds #-}
module B where
import A
g1 :: ()
g1 = t1FunA $ \x ->
let y = MkT1
in t1FunB x y
g2 :: ()
g2 = t2FunA $ \x ->
let y = MkT2
in t2FunB x y
```
The `A` module defines two data types, `T1` and `T2`, as well as some functions which use them. The only difference between `T1` and `T2` is that the latter uses visible dependent quantification while the former does not. The `B` module uses these functions in a relatively straightforward way. Note that `B` does _not_ enable `PolyKinds` (I distilled this from a `cabal` project which uses `Haskell2010`).
What's curious about this is that while both `g1` and `g2` will typecheck on GHC 9.0.2, only `g1` typechecks on GHC 9.2.1. On the other hand, `g2` will fail to typecheck in GHC 9.2.1:
```
$ ghc-9.2.1 B.hs
[1 of 2] Compiling A ( A.hs, A.o )
[2 of 2] Compiling B ( B.hs, B.o )
B.hs:14:18: error:
• Couldn't match type ‘a’ with ‘*’
Expected: T2 a
Actual: T2 (*)
‘a’ is a rigid type variable bound by
a type expected by the context:
forall a. T2 a -> ()
at B.hs:(12,15)-(14,18)
• In the second argument of ‘t2FunB’, namely ‘y’
In the expression: t2FunB x y
In the expression: let y = MkT2 in t2FunB x y
• Relevant bindings include x :: T2 a (bound at B.hs:12:16)
|
14 | in t2FunB x y
| ^
```
I'm not confident enough to claim with 100% certainty that this is a regression, since the use of `NoPolyKinds` might be throwing a wrench into things. Indeed, enabling `PolyKinds` is enough to make the program accepted again. Still, the fact that this _only_ fails if the data type uses visible dependent quantification (and _only_ with GHC 9.2.1) is rather strange, so I wanted to file an issue to ask people more knowledgeable in this space than I am.https://gitlab.haskell.org/ghc/ghc/-/issues/21041Check laziness of Coercion in the Reduction type2023-12-04T15:08:50ZRichard Eisenbergrae@richarde.devCheck laziness of Coercion in the Reduction typeThe `Coercion` stored in a `Reduction` is lazy in order to work with Derived constraints. However, once !5899 lands, Derived constraints will be a part of history. We should then check to see if making this coercion strict would yield a ...The `Coercion` stored in a `Reduction` is lazy in order to work with Derived constraints. However, once !5899 lands, Derived constraints will be a part of history. We should then check to see if making this coercion strict would yield a performance improvement.https://gitlab.haskell.org/ghc/ghc/-/issues/21077GHC 9.2.1 typechecking regression with RankNTypes, TemplateHaskell, and compo...2023-08-04T17:02:49ZRyan ScottGHC 9.2.1 typechecking regression with RankNTypes, TemplateHaskell, and compound expressions_(Originally spun off from https://gitlab.haskell.org/ghc/ghc/-/issues/21038#note_407457)_
The `crux-llvm` library (specifically, [this code](https://github.com/GaloisInc/crucible/blob/e1308319eef8e0fcb55ed04df7eb2e9d5e87aac5/crux-llvm/..._(Originally spun off from https://gitlab.haskell.org/ghc/ghc/-/issues/21038#note_407457)_
The `crux-llvm` library (specifically, [this code](https://github.com/GaloisInc/crucible/blob/e1308319eef8e0fcb55ed04df7eb2e9d5e87aac5/crux-llvm/src/Crux/LLVM/Overrides.hs#L149-L153)) typechecks on GHC 9.0.2 and earlier, but fails to typecheck with GHC 9.2.1. I made an attempt to minimize the issue in #21038, but after trying again with that patch, I discovered that `crux-llvm` _still_ does not typecheck. It turns out that my minimization of the issue was a bit too minimal. Here is an example that better illustrates what is going on:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
module Bug where
data Foo = MkFoo () (forall a. a -> a)
worksOnAllGHCs1 :: Foo
worksOnAllGHCs1 = MkFoo () (\x -> x)
worksOnAllGHCs2 :: Foo
worksOnAllGHCs2 = MkFoo () $ \x -> x
worksOnAllGHCs42 :: Foo
worksOnAllGHCs42 = (MkFoo ()) $ \x -> x
doesn'tWorkOnGHC9'2 :: Foo
doesn'tWorkOnGHC9'2 = $([| MkFoo () |]) $ \x -> x
```
As the names suggest, all of the things functions will typecheck on GHC 9.0.2 and earlier. The `worksOnAllGHCs{1,2,3}` functions will typecheck on GHC 9.2.1, but `doesn'tWorkOnGHC9'2` will not:
```
$ ghc-9.2.1 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o, Bug.dyn_o )
Bug.hs:17:24: error:
• Couldn't match type: forall a. a -> a
with: p0 -> p0
Expected: (p0 -> p0) -> Foo
Actual: (forall a. a -> a) -> Foo
• In the first argument of ‘($)’, namely ‘(MkFoo ())’
In the expression: (MkFoo ()) $ \ x -> x
In an equation for ‘doesn'tWorkOnGHC9'2’:
doesn'tWorkOnGHC9'2 = (MkFoo ()) $ \ x -> x
|
17 | doesn'tWorkOnGHC9'2 = $([| MkFoo () |]) $ \x -> x
| ^^^^^^^^^^^^^^^^
```
The commit which introduced this regression is 9632f413dc90f39bc64586c064805f515a672ca0 (`Implement Quick Look impredicativity`).
Note that unlike the example in #21038, the expression being spliced isn't a simple identifier (i.e., a "head", to use Quick Look terminology), but rather a compound expression. @simonpj suggests [the following fix](https://gitlab.haskell.org/ghc/ghc/-/issues/21038#note_407705):
> Ah yes. Hmm. Reflecting on this, I think the Right Thing is *to treat a splice that is run in the renamer (i.e. an untyped TH splice) as using the "HsExpansion" mechanism*. See `Note [Handling overloaded and rebindable constructs]` in GHC.Tc.Rename.Expr.
>
> That is, the splice `$(expr)` turns into `HsExpanded $(expr) <result-of-running-splice>`. After all, it really *is* an expansion! Then the stuff in the type checker will deal smoothly with application chains. See `Note [Looking through HsExpanded]` in GHC.Tc.Gen.Head.
>
> In principle that should be pretty easy. But `Note [Delaying modFinalizers in untyped splices]` in GHC.Rename.Splice is a painful wart that will hurt us here.
>
> * Where might we store these modFinalizdrs in the HsExpanded? Maybe in the first (original expression) field?
> * Actually I think I favour separating them out entirely into a new extension constructor for `HsExpr GhcRn`. Currenlty we have
>
> ```
> type instance XXExpr GhcRn = HsExpansion (HsExpr GhcRn) (HsExpr GhcRn)
> type instance XXExpr GhcTc = XXExprGhcTc
> ```
>
> We could instead have
>
> ```
> type instance XXExpr GhcRn = XXExprGhcRn
>
> data XXExprGhcRn = ExpansionRn (HsExpansion (HsExpr GhcRn) (HsExpr GhcRn))
> | AddModFinalizedrs ThModFinalizers (HsExpr GhcRn)
> ```
>
> In exchange we can get rid of `HsSpliced` altogether.
> * We still need to call `addModFinalizersWithLclEnv` on those finalisers; so it looks as if we'd need to make `splitHsApps` monadic. That's a pain, but not actually difficult.
>
> I'm not certain of this. But *something* along these lines seems like the right solution.Ryan ScottRyan Scotthttps://gitlab.haskell.org/ghc/ghc/-/issues/21088Inconsistent instantiation of inferred type variables when they don't all com...2022-03-03T08:25:55Zsheafsam.derbyshire@gmail.comInconsistent instantiation of inferred type variables when they don't all come firstCurrently, in `GHC.Tc.Gen.App.tcInstFun`, when we are instantiating inferred type variables (for example for `:type` in GHCi), we instantiate only the inferred type variables that appear before any other quantified type variables.
Examp...Currently, in `GHC.Tc.Gen.App.tcInstFun`, when we are instantiating inferred type variables (for example for `:type` in GHCi), we instantiate only the inferred type variables that appear before any other quantified type variables.
Example:
```haskell
{r1 :: RuntimeRep} (a :: TYPE r1) {r2 :: RuntimeRep} (b :: TYPE r2)
```
Here we will instantiate `r1`, but not `r2` because `r2` comes after `a` which we are not instantiating because `a` is not an inferred type variable (recall that we are in the case in which `inst_fun = inst_inferred`). This means that `:type` in GHCi could end up reporting a type like
```haskell
forall a {r2 :: RuntimeRep} (b :: TYPE r2)
```
This is just too confusing, in my opinion.
How to fix this?
1. Initially I thought we might make an effort to re-arrange the type variables and still instantiate `r2` even though it appears after `a`. However, as this isn't possible in general (e.g. if the kind of `r2` mentioned `a`, we wouldn't be able to re-arrange the telescope), and @rae dissuaded me from pursuing it further.
2. @mpickering instead suggested that we don't instantiate any inferred type variables when we run into such a situation. This is what I will be pursuing; it only entails adding a single additional check that there are no more splittable quantified variables (in `GHC.Tc.Gen.App.tcInstFun.go1`).sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/21116ASSERT failed! on T161352023-07-18T08:49:00ZMatthew PickeringASSERT failed! on T16135```
{-# LANGUAGE ExistentialQuantification, ApplicativeDo #-}
module Bug where
data T f = forall a. MkT (f a)
runf :: forall f. Functor f => IO (T f)
runf = do
return ()
MkT fa <- runf
return $ MkT fa
```
Leads to asserti...```
{-# LANGUAGE ExistentialQuantification, ApplicativeDo #-}
module Bug where
data T f = forall a. MkT (f a)
runf :: forall f. Functor f => IO (T f)
runf = do
return ()
MkT fa <- runf
return $ MkT fa
```
Leads to assertion failure
```
ghc: panic! (the 'impossible' happened)
GHC version 9.3.20220221:
ASSERT failed!
2
1
a_aEs[tau:1]
a_aEe[ssk:2]
Call stack:
CallStack (from HasCallStack):
massertPpr, called at compiler/GHC/Tc/Utils/TcMType.hs:1027:10 in ghc:GHC.Tc.Utils.TcMType
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```
Related to #21113https://gitlab.haskell.org/ghc/ghc/-/issues/21126Definition of heterogeneous equality rejected unless using a SAKS2022-04-07T16:01:28Zsheafsam.derbyshire@gmail.comDefinition of heterogeneous equality rejected unless using a SAKSThe following definitions of heterogeneous equality are rejected on HEAD:
```haskell
data (a :: k1) :~: (b :: k2) where
HRefl :: a :~~: a
```
```
error:
* Different names for the same type variable: `k1' and `k2'
* In the da...The following definitions of heterogeneous equality are rejected on HEAD:
```haskell
data (a :: k1) :~: (b :: k2) where
HRefl :: a :~~: a
```
```
error:
* Different names for the same type variable: `k1' and `k2'
* In the data declaration for `:~~:'
|
| data (a :: k1) :~~: (b :: k2) where
| ^^^^^^^^^^^^^^^^^^^^^^
```
```haskell
data (:~~:) :: k1 -> k2 -> Type where
HRefl :: a :~~: a
```
```
error:
* Different names for the same type variable: `k1' and `k2'
* In the data declaration for `:~~:'
|
| data (:~~:) :: k1 -> k2 -> Type where
| ^^^^^^^^
```
Note that this remains true even if one enables `-XCUSKs`, so this doesn't fit the diagnostic of https://gitlab.haskell.org/ghc/ghc/-/issues/20752#note_394357.
The only way to get this accepted is to write a standalone kind signature:
```haskell
type (:~~:) :: k1 -> k2 -> Type
data a :~~: b where
HRefl :: a :~~: a
```
It seems to me that the "different names for the same type variable" check is overly-eager for GADTs. In particular, the following is also rejected:
```haskell
data (:~~:) :: k1 -> k2 -> Type where
NotHRefl :: forall k1 k2 (a :: k1) (b :: k2). a :~~: b
HRefl :: a :~~: a
```
```
error:
* Different names for the same type variable: `k1' and `k2'
* In the data declaration for `:~~:'
|
| data (:~~:) :: k1 -> k2 -> Type where
| ^^^^^^^^
```
I don't know how GHC concludes that `k1` and `k2` must refer to the same kind variable there.9.4.1sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/21139Unfoldings in interface files are sucked in too eagerly2022-02-26T12:48:59ZSimon Peyton JonesUnfoldings in interface files are sucked in too eagerlyThis ticket is a standalone report of a discovery we made in a merge request discussion !6735; specifically [this comment](https://gitlab.haskell.org/ghc/ghc/-/merge_requests/6735#note_389262).
There is a long-standing bug in typecking...This ticket is a standalone report of a discovery we made in a merge request discussion !6735; specifically [this comment](https://gitlab.haskell.org/ghc/ghc/-/merge_requests/6735#note_389262).
There is a long-standing bug in typecking the unfoldings from interface files.
* A call to `hasNoBinding` will force the Id's `Unfolding`
* Because of a bug in `tcUnfolding` (see below), that will force the thunk created by `tcPragExpr`
* And that lint the rhs before returning it
* And Linting will call `hasNoBinding` on Ids mentioned in the rhs
* Which will force their unfoldings
* And so on.
Never mind loops -- this forces way too much stuff to get sucked in from interface files -- essentially the transitive closure of everything.
Other notes:
* **TODO** `tcPragExpr` should be renamed to be `tcUnfoldingRhs`.
* `Note [Linting Unfoldings from Interfaces]` is nothing to do with loops. Consider this decl in an interface file M.hi:
```
f = \x. let y = blah in blah2
```
When we Lint f's unfolding we will Lint y's unfolding too: see
```
lintLetBind top_lvl rec_flag binder rhs rhs_ty
= do { ...
; ; addLoc (UnfoldingOf binder) $
lintIdUnfolding binder binder_ty (idUnfolding binder)
```
So there is no point in *also* Linting y's unfolding during `tcIfaceExpr` on f's RHS. That's all. **TODO** Could the Note be make clearer?
* I don't see how `idUnfolding` vs `realIdUnfolding` makes the slightest difference. The difference is only that the former consults OccInfo first.
The Real Bug is here:
```
tcUnfolding toplvl name _ info (IfCoreUnfold stable if_expr)
= do { uf_opts <- unfoldingOpts <$> getDynFlags
; mb_expr <- tcPragExpr False toplvl name if_expr
; ...
; return $ case mb_expr of
Nothing -> NoUnfolding
Just expr -> mkFinalUnfolding uf_opts unf_src strict_sig expr
}
```
Notice that to choose between `NoUnfolding` and `CoreUnfolding` (which is returned by `mkFinalUnfolding`), we force `mb_expr`. **ALAS**! That is the very thunk we are trying delay forcing!
I think we should always return a `CoreUnfolding` thus:
```
; return $ mkFinalUnfolding uf_opts unf_src strict_sig
(case mb_expr of { Just e -> e; Nothing -> panic })
```
Or, more directly, use `forkM` (not `forkM_maybe`) in `tcPragExpr`.
This is just what Sam suggests:
> What I am trying to do currently is to architect `tcUnfolding` so that it immediately returns an unfolding which we can inspect to obtain the value of `hasNoBinding`
Why do we *ever* use `forkM_maybe`? There is a mysterious comment:
```
forkM_maybe doc thing_inside
= do { unsafeInterleaveM $
do { traceIf (text "Starting fork {" <+> doc)
; mb_res <- tryM thing_inside ;
case mb_res of
Right r -> do { traceIf (text "} ending fork" <+> doc)
; return (Just r) }
Left exn -> do {
-- Bleat about errors in the forked thread, if -ddump-if-trace is on
-- Otherwise we silently discard errors. Errors can legitimately
-- happen when compiling interface signatures (see tcInterfaceSigs)
ifOptM Opt_D_dump_if_trace
(print_errs (hang (text "forkM failed:" <+> doc)
4 (text (show exn))))
```
I have no idea what these "legitimate" errors are. git-blame tells me that this
comment dates back to before this 2003 commit:
```
commit 98688c6e8fd33f31c51218cf93cbf03fe3a5e73d
Author: simonpj <unknown>
Date: Thu Oct 9 11:59:43 2003 +0000
[project @ 2003-10-09 11:58:39 by simonpj]
-------------------------
GHC heart/lung transplant
-------------------------
This major commit changes the way that GHC deals with importing
types and functions defined in other modules, during renaming and
typechecking. On the way I've changed or cleaned up numerous other
things, including many that I probably fail to mention here.
```
Moreover this commit *removes* `tcInterfaceSigs`. So I think it's historical.
**Proposal (TODO)**: get rid of `forkM_maybe`, and use `forkM` all the time.
I think that will solve our problem. But let's leave some careful Notes to explain
this. Notably, it's important that `mkFinalUnfolding` and friends all return
a `CoreUnfolding` *without forcing the unfolding rhs*.
All clear?https://gitlab.haskell.org/ghc/ghc/-/issues/21158Record update typing is wrong2022-05-26T07:43:22ZSimon Peyton JonesRecord update typing is wrongConsider this
```
type family F a
data T b = MkT { x :: [Int], y :: [F b] }
emptyT :: T b
emptyT = MkT [] []
foo1 :: [Int] -> T b
foo1 newx = emptyT { x = newx }
foo2 :: [Int] -> T b
foo2 newx = case emptyT of MkT x y -> MkT newx y...Consider this
```
type family F a
data T b = MkT { x :: [Int], y :: [F b] }
emptyT :: T b
emptyT = MkT [] []
foo1 :: [Int] -> T b
foo1 newx = emptyT { x = newx }
foo2 :: [Int] -> T b
foo2 newx = case emptyT of MkT x y -> MkT newx y
```
According to [the Haskell report](https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-490003.15), `foo1` and `foo2` should behave the same. But they don't: `foo2` is rejected with
```
Foo.hs:29:49: error:
• Couldn't match type: F b0
with: F b
Expected: [F b]
Actual: [F b0]
NB: ‘F’ is a non-injective type family
The type variable ‘b0’ is ambiguous
• In the second argument of ‘MkT’, namely ‘y’
In the expression: MkT newx y
In a case alternative: MkT x y -> MkT newx y
• Relevant bindings include
y :: [F b0] (bound at Foo.hs:29:35)
foo2 :: [Int] -> T b (bound at Foo.hs:29:1)
|
29 | foo2 newx = case emptyT of MkT x y -> MkT newx y
| ^
```
And indeed that makes sense: becuase `F` is a type family, we have no way to know at what type to instantiate `emptyT`.
So why does `foo1` work? It's because of this code in GHC.Tc.Gen.Expr, in the `RecordUpd` case of `tcExpr`:
```
-- 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
--
; let fixed_tvs = getFixedTyVars upd_fld_occs con1_tvs relevant_cons
is_fixed_tv tv = tv `elemVarSet` fixed_tvs
```
Those "fixed" tyvars are the ones that GHC thinks are going to be the same in "before" and "after" -- and it used *all the free vars* of unaffected fields (in this case the field `y`).
So `b` is treated as "fixed".
But that is not what the report says; and it would be reasonably complicated to specify. The simplest thing is to regard this a bug, which leads GHC to accept too many programs. It is not hard to fix `foo2`:
```
foo2 :: forall b. [Int] -> T b
foo2 newx = case (emptyT :: T b) of MkT x y -> MkT newx y
```
This came up during @CarrieMY's work on !7320/#18802. It turns out that GHC itself uses this idiom in GHC.Hs.Utils:
```
mkRecStmt anns stmts = (emptyRecStmt' anns) { recS_stmts = stmts }
```
When we desugar record update in the renamer, this rejected for the reasons above.https://gitlab.haskell.org/ghc/ghc/-/issues/21199(GHC 9.2.2) Impossible happened...2022-07-28T10:15:10ZAdam Conner-Sax(GHC 9.2.2) Impossible happened...## Summary
GHC 9.2.2 compiler reports "The impossible happened"
```
ghc-9.2.2: panic! (the 'impossible' happened)
(GHC version 9.2.2:
mightEqualLater finds an unbound cbv
cbv_a1TC[cbv:1]
[]
Call stack:
CallStack (from Has...## Summary
GHC 9.2.2 compiler reports "The impossible happened"
```
ghc-9.2.2: panic! (the 'impossible' happened)
(GHC version 9.2.2:
mightEqualLater finds an unbound cbv
cbv_a1TC[cbv:1]
[]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:181:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Tc/Solver/Monad.hs:2587:16 in ghc:GHC.Tc.Solver.Monad
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```
## Steps to reproduce
Build the repo (https://github.com/adamConnerSax/impossible922) with ghc 9.2.2
## Expected behavior
I expect it to build (as it does with ghc 8.10.7)
## Environment
GHC 9.2.2 (optionally ghc 8.10.7), cabal 3.6.2 (all installed with ghcup)
Optional:
* Operating system: MacOs 12.2.1
* System Architecture: Mac Pro (tower, late 2013)9.2.3https://gitlab.haskell.org/ghc/ghc/-/issues/21206lookupIdSubst panic with indexed monad2024-02-05T22:55:26ZTobias HasloplookupIdSubst panic with indexed monadSee also
* #22788
* #23147
## Summary
Compiling causes a panic. I initially observed this with GHC 9.2.1
I noticed that the panic looks similar to the panic from #20820, for which there is the fix !7664. Since !7664 has not been mer...See also
* #22788
* #23147
## Summary
Compiling causes a panic. I initially observed this with GHC 9.2.1
I noticed that the panic looks similar to the panic from #20820, for which there is the fix !7664. Since !7664 has not been merged yet, I tried compiling the code with a [CI-build that contains the fix](https://gitlab.haskell.org/ghc/ghc/-/jobs/959784). That CI-build panics too.
## Steps to reproduce
Compile this cabal project with a recent GHC:
[lookupidsubst-panic.zip](/uploads/edbf21a3bd8d0ba7e0a252863532d90d/lookupidsubst-panic.zip)
```
PS C:\Users\Tobias\Documents\Uni\haskell\lookupidsubst-panic> cabal build --with-compiler="C:\Program Files\ghc-9.3.20220225-x86_64-unknown-mingw32\bin\ghc-9.3.20220225.exe"
Resolving dependencies...
Build profile: -w ghc-9.3.20220225 -O1
In order, the following will be built (use -v for more details):
- lookupidsubst-panic-0.1.0.0 (exe:lookupidsubst-panic) (first run)
Configuring executable 'lookupidsubst-panic' for lookupidsubst-panic-0.1.0.0..
Preprocessing executable 'lookupidsubst-panic' for lookupidsubst-panic-0.1.0.0..
Building executable 'lookupidsubst-panic' for lookupidsubst-panic-0.1.0.0..
<no location info>: warning: [-Wmissing-home-modules]
These modules are needed for compilation but not listed in your .cabal file's other-modules:
Base Demonad TypeState
[1 of 5] Compiling Base ( app\Base.hs, C:\Users\Tobias\Documents\Uni\haskell\lookupidsubst-panic\dist-newstyle\build\x86_64-windows\ghc-9.3.20220225\lookupidsubst-panic-0.1.0.0\x\lookupidsubst-panic\build\lookupidsubst-panic\lookupidsubst-panic-tmp\Base.o )
[2 of 5] Compiling Demonad ( app\Demonad.hs, C:\Users\Tobias\Documents\Uni\haskell\lookupidsubst-panic\dist-newstyle\build\x86_64-windows\ghc-9.3.20220225\lookupidsubst-panic-0.1.0.0\x\lookupidsubst-panic\build\lookupidsubst-panic\lookupidsubst-panic-tmp\Demonad.o )
[3 of 5] Compiling TypeState ( app\TypeState.hs, C:\Users\Tobias\Documents\Uni\haskell\lookupidsubst-panic\dist-newstyle\build\x86_64-windows\ghc-9.3.20220225\lookupidsubst-panic-0.1.0.0\x\lookupidsubst-panic\build\lookupidsubst-panic\lookupidsubst-panic-tmp\TypeState.o )
[4 of 5] Compiling Main ( app\Main.hs, C:\Users\Tobias\Documents\Uni\haskell\lookupidsubst-panic\dist-newstyle\build\x86_64-windows\ghc-9.3.20220225\lookupidsubst-panic-0.1.0.0\x\lookupidsubst-panic\build\lookupidsubst-panic\lookupidsubst-panic-tmp\Main.o )
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.3.20220225:
lookupIdSubst
$dNum_a26l
InScope {i_a25Y $dDemonad_a269 $creturnIx_a2gd $cbindIx_a2gY
$cseqIx'_a2ir $krep_a2kH $krep_a2kI $krep_a2kJ $krep_a2kK
$krep_a2kL $krep_a2kM $krep_a2kN $krep_a2kO $krep_a2kP $krep_a2kQ
$krep_a2kR $krep_a2kS $krep_a2kT $krep_a2kU $krep_a2kV $krep_a2kW
$krep_a2kX $krep_a2kY $krep_a2kZ $krep_a2l0 $krep_a2l1 $krep_a2l2
$krep_a2l3 $krep_a2l4 $krep_a2l5 $krep_a2l6 $krep_a2l7 $krep_a2l8
$krep_a2l9 $krep_a2la $krep_a2lb $krep_a2lc $krep_a2ld $krep_a2le
$krep_a2lf runSt add1 solve1 val1 $tc'Satisfied $tc'Unsatisfied
$tc'Interrupted $tcTerminatedSolverRun $tc'MkStRes $tcStRes
$tc'MkSt $tcSt $fDemonadkSt $tc'MkVarVal $tcVarVal $trModule}
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler\\GHC\\Utils\\Panic.hs:182:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler\GHC\Core\Subst.hs:260:17 in ghc:GHC.Core.Subst
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```
## Expected behavior
I expect the code to compile successfully. Alternatively I expect a sensible error message but not a panic.
## Environment
* GHC version used: https://gitlab.haskell.org/ghc/ghc/-/jobs/959784
* Operating System: Windowshttps://gitlab.haskell.org/ghc/ghc/-/issues/21208GHC doesn't notice some overlapping instances (regression)2022-12-20T12:31:30ZRichard Eisenbergrae@richarde.devGHC doesn't notice some overlapping instances (regression)If I have
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
module Bug6 where
type family F a
inject :: a -> F a
inject = undefined
class C a where
meth :: a -> ()
instance C a where
meth _ = ()
g :: C a =...If I have
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
module Bug6 where
type family F a
inject :: a -> F a
inject = undefined
class C a where
meth :: a -> ()
instance C a where
meth _ = ()
g :: C a => a -> ()
g x = meth (inject x)
```
then GHC 8.10.7 will say
```
• Overlapping instances for C (F a) arising from a use of ‘meth’
Matching instances:
instance C a
-- Defined at /Users/rae/pCloud Drive/work/temp/Bug6.hs:14:10
There exists a (perhaps superclass) match:
from the context: C a
bound by the type signature for:
g :: forall a. C a => a -> ()
at /Users/rae/pCloud Drive/work/temp/Bug6.hs:17:1-19
(The choice depends on the instantiation of ‘a’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
• In the expression: meth (inject x)
In an equation for ‘g’: g x = meth (inject x)
```
I think this is quite sensible behavior: the local `C a` might apply, if `F a ~ a` for some `a`, overriding the global `instance forall a. C a`.
But GHC 9.2.1 and HEAD accept!9.2.3Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/21209Quantified constraint blocks functional dependency2022-03-25T21:37:14ZRichard Eisenbergrae@richarde.devQuantified constraint blocks functional dependencyConsider
```hs
{-# LANGUAGE FunctionalDependencies, QuantifiedConstraints, AllowAmbiguousTypes #-}
module Bug2 where
class C a b | a -> b where
method :: a -> b -> ()
class Truth
instance Truth
f :: (C a b) => a -> ()
f x = method...Consider
```hs
{-# LANGUAGE FunctionalDependencies, QuantifiedConstraints, AllowAmbiguousTypes #-}
module Bug2 where
class C a b | a -> b where
method :: a -> b -> ()
class Truth
instance Truth
f :: (C a b) => a -> ()
f x = method x undefined
g :: (Truth => C a b) => a -> ()
g x = method x undefined
```
`f` is accepted, while `g` is not (in every version of GHC I tested, including HEAD), due to ambiguity of `b` in the call to `method`. But, really, this should be accepted, because the premise of the quantified constraint in the type of `g` is satisfied. The functional dependency should thus choose the type of `undefined` to be `b`.https://gitlab.haskell.org/ghc/ghc/-/issues/21239Add syntactic equality relation2022-04-28T23:29:28Zsheafsam.derbyshire@gmail.comAdd syntactic equality relationIn several places, it would be useful to have a syntactic equality relation, `~S#`.
* Under this relation, two types are equal if they respond equal to `tcEqType`, up to zonking.
(This means: no rewriting, but we can zonk and look thr...In several places, it would be useful to have a syntactic equality relation, `~S#`.
* Under this relation, two types are equal if they respond equal to `tcEqType`, up to zonking.
(This means: no rewriting, but we can zonk and look through type synonyms.)
* The evidence for `t1 ~S# t2` is always Refl.
With such an equality relation, we could:
* **Get rid of `IsRefl#`**. Currently, the representation polymorphism checks emit a nominal equality `ki ~# concrete_tv`, and when we don't support rewriting (because of [PHASE 1 of `FixedRuntimeRep`](https://gitlab.haskell.org/ghc/ghc/-/wikis/FixedRuntimeRep)) we additionally emit `IsRefl# ki concrete_tv`. Instead, we should syntactically unify `ki` with `concrete_tv` in PHASE 1.
* **Enforce a specific runtime rep**. Suppose we want to enforce that a type `ty :: TYPE rr` has a specific runtime representation `specific_rr`, without any coercions needed, (e.g. `LiftedRep` if we want to enforce liftedness). Then we can syntactically unify `rr` with `specific_rr`. Example of when this is useful: `\x -> (x, True)`. At the lambda, `x` comes into scope with type `x :: alpha :: TYPE rr`. Later we find that it must be lifted because it's an argument to the tuple.
## Implementation
A useful property of `(~S#)` is that it can be solved or refuted without ever generating any constraints. So this should **NOT** be a new constructor of `EqRel`, because we have no need for a syntactic equality predicate. All we need is a counterpart to `uType` that works at the syntactic level, doing unification as it goes, and *never deferring to the main constraint solver*.sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/21289Type-changing record update ignores type families2022-05-26T07:42:42ZRichard Eisenbergrae@richarde.devType-changing record update ignores type familiesI would like this to compile:
```hs
type family F (a :: Bool)
type instance F True = Int
type instance F False = Int
type family G (a :: Bool)
type instance G True = Int
type instance G False = Bool
data Rec a = MkR { konst :: F a
...I would like this to compile:
```hs
type family F (a :: Bool)
type instance F True = Int
type instance F False = Int
type family G (a :: Bool)
type instance G True = Int
type instance G False = Bool
data Rec a = MkR { konst :: F a
, change :: G a }
ch :: Rec True -> Rec False
ch r = r { change = False }
```
The `ch` function does a type-changing record update. Normally, a type-changing record update can be written only when all fields that mention the changing type variable are updated. And `ch` does not update `konst`, whose type mentions `a`. But it's OK, actually: because `F True` (old type) and `F False` (new type) are actually both `Int`, all is well. Yet GHC rejects.
Unlike some bugs I report, this one is from a Real Use Case. (I have a practical, fancy-typed library I'm building that wants to ensure that a particular record-update updates certain fields.)
While in town, should probably also fix #10856 and transitively #2595 (which, I think, is effectively a dup of #10856).https://gitlab.haskell.org/ghc/ghc/-/issues/21346GHC no longer instantiates representation-polymorphic newtype constructors2022-06-10T10:36:35Zsheafsam.derbyshire@gmail.comGHC no longer instantiates representation-polymorphic newtype constructorsConsider the following program:
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UnliftedNewtypes #-}
import GHC.Exts
newtype N r (a :: TYPE r) = MkN a
foo :: Int# -> N IntRep I...Consider the following program:
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UnliftedNewtypes #-}
import GHC.Exts
newtype N r (a :: TYPE r) = MkN a
foo :: Int# -> N IntRep Int#
foo i = MkN i
```
On GHC 9.2, the output of `-ddump-ds-preopt` is:
```haskell
foo = \ (i :: Int#) -> (\ (ds :: Int#) -> MkN @'IntRep @Int# ds) i
```
That is, we have instantiated the representation-polymorphic `MkN :: forall r (a :: TYPE r) . a -> N r a`, with `MkN @IntRep @Int#`.
However, on GHC HEAD, we get:
```haskell
foo = \ (i :: Int#) -> (\ @(r :: RuntimeRep) @(a :: TYPE r) (ds :: a) -> MkN @r @a ds) i
```
here we have a representation-polymorphic binder `ds :: a`!
I think this issue was introduced in !5640. There used to be logic in `tc_infer_id` to instantiate a representation-polymorphic data constructor, but that logic seems to have vanished entirely, and the new `tcInferDataCon` function does not do any instantiation. It's left with the original argument types, and thus `dsConLike` gets passed argument types which don't have a fixed runtime representation.
I think we should have an invariant that the argument types stored in `ConLikeTc` have a syntactically fixed RuntimeRep, which is necessary as they are the types of variables bound in a lambda (created by `dsConLike`), and enforce it by instantiating the newtype constructor.
This issue is causing me trouble with the implementation of PHASE 2 of FixedRuntimeRep.Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/21377simple_app fails to beta-reduce through casts2022-06-01T19:36:42Zsheafsam.derbyshire@gmail.comsimple_app fails to beta-reduce through casts`simple_app` sometimes misses beta reduction opportunities because of intervening casts.
See also #21346
## Example 1: casted lambda
`simple_app` does not reduce the application of a casted lambda abstraction to an argument, e.g. `(la...`simple_app` sometimes misses beta reduction opportunities because of intervening casts.
See also #21346
## Example 1: casted lambda
`simple_app` does not reduce the application of a casted lambda abstraction to an argument, e.g. `(lam |> co) arg`. This fails to beta reduce because `simple_app` does not look through casts to find lambda expressions. Simply calling `exprIsLambda_maybe` instead of pattern matching on `Lam` in `simple_app` allows beta reduction to take place.
## Example 2: lambda, argument, cast, argument
`simple_app` fails to collect arguments through casts, e.g. in `( (lam arg1) |> co ) arg2` we will beta reduce `lam arg1` but then fail to beta reduce the application of the result to the second argument. This problem persists after fixing the previous issue. I'm not sure what the correct solution is, something like the following perhaps (after the case in `simple_app` that deals with lambdas, as we want to push the coercion through the lambda and not into the arguments in that case):
```haskell
simple_app env (Cast fun co) args
| (envs, as) <- unzip args
, Just (as, mco) <- pushCoArgs co as
= mkCastMCo (simple_app env fun $ zip envs as) mco
```
## Why this matters
We rely on the simple optimiser to beta reduce away the representation-polymorphic lambdas introduced by the desugaring of data constructors, as explained in Note [Typechecking data constructors] in `GHC.Tc.Gen.Head`. If we don't properly beta-reduce these representation-polymorphic lambdas, we violate the representation polymorphism invariants, which could cause GHC to crash (e.g. on `typePrimRep`).
I ran into the above two examples in test cases `T20363`/`T20363b`, trying to allow this test case to compile by using [PHASE 2 of the `FixedRuntimeRep` plan](https://gitlab.haskell.org/ghc/ghc/-/wikis/FixedRuntimeRep#phase-2).
## Alternatives
I am still wondering whether we can figure out another way to handle the multiplicities in data constructors that would avoid having to perform this dodgy eta expansion. Perhaps @monoidal @rae have some ideas about this, because I really don't like having to rely on fragile optimisations to simplify away invalid Core. I would encourage you to think about `hasFixedRuntimeRep_remainingValArgs`: this function precisely checks that we can eta expand, so we should be able to use the information therein to actually perform the correct eta expansion!
I have the following kind of examples in mind here:
```haskell
type family RR :: RuntimeRep where
RR = LiftedRep
type family C :: TYPE RR where
C = Char
newtype T :: TYPE RR where
MkT :: C -> T
g :: Char -> T
g = MkT
-- Here we should eta-expand 'MkT' to
--
-- \ (ds :: (C |> TYPE RR[O])) -> ...
--
-- and not
--
-- \ (ds :: C) -> ...
--
-- (Even though 'C' is the 'origArgTy' stored in the 'MkT' data constructor,
-- it's not what we should use for eta expansion.)
type Q :: forall (r :: RuntimeRep). TYPE r -> TYPE r
newtype Q a where
MkQ :: forall (r :: RuntimeRep) (a :: TYPE r). a -> MkQ a
q = MkQ @IntRep
-- Here I believe we need to handle the whole application, as if
-- we simply eta-expanded 'MkQ' to lam = /\ (a :: TYPE IntRep). \ (ds :: a) -> ...
-- then the type application "lam @IntRep" wouldn't make sense.
```Arnaud SpiwackKrzysztof GogolewskiArnaud Spiwackhttps://gitlab.haskell.org/ghc/ghc/-/issues/21404decideMonoTyVars doesn't handle coercion variables in "candidates"2022-04-27T17:38:37Zsheafsam.derbyshire@gmail.comdecideMonoTyVars doesn't handle coercion variables in "candidates"In `decideMonoTyVars` we find:
```haskell
mono_tvs0 = filterVarSet (not . isQuantifiableTv tc_lvl) $
tyCoVarsOfTypes candidates
...
co_vars = coVarsOfTypes (psig_tys ++ taus)
mono_tvs1 = mono_tvs0 `unionVarSet` co_var_tvs
.....In `decideMonoTyVars` we find:
```haskell
mono_tvs0 = filterVarSet (not . isQuantifiableTv tc_lvl) $
tyCoVarsOfTypes candidates
...
co_vars = coVarsOfTypes (psig_tys ++ taus)
mono_tvs1 = mono_tvs0 `unionVarSet` co_var_tvs
...
mono_tvs2 = closeWrtFunDeps non_ip_candidates mono_tvs1
```
Note that `closeWrtFunDeps` expects a set of type variables closed over kinds. However, `mono_tvs1` doesn't seem to be closed over kinds, in general:
1. `tyCoVarsOfTypes` is deep, so `tyCoVarsOfTypes candidates` is closed over kinds.
2. We filter out some variables using `isQuantifiableTv`. How do we know this set is still closed over kinds? In particular, we might have kept a coercion variable but not the type variables found in its kind.
I ran into the following example while working on a patch:
Candidates:
- `{co} :: gamma[conc] ~# F`
- `alpha[tau:1] ~# (beta[tau:1] |> TYPE {co})`
At `TcLevel` 0, `mono_tvs0 = {co}`, `closeOverKinds mono_tvs0 = {co, gamma}`.
@rae, what am I missing? Is the above collection of candidates somehow ill-formed, i.e. doesn't uphold some invariant required to pass it to `decideMonoTyVars`?https://gitlab.haskell.org/ghc/ghc/-/issues/21405Assertion in reportWanteds is too strict2023-02-01T08:38:59Zsheafsam.derbyshire@gmail.comAssertion in reportWanteds is too strictThere's an assertion in `reportWanteds` that checks that we aren't suppressing all the errors.
```haskell
-- This check makes sure that we aren't suppressing the only error that will
-- actually stop compilation
; ...There's an assertion in `reportWanteds` that checks that we aren't suppressing all the errors.
```haskell
-- This check makes sure that we aren't suppressing the only error that will
-- actually stop compilation
; massert $
null simples || -- no errors to report here
any ignoreConstraint simples || -- one error is ignorable (is reported elsewhere)
not (all ei_suppress tidy_items) -- not all errors are suppressed
```
This is in the context of "Wanteds rewrite Wanteds", where we should always have one non-rewritten Wanted to report to the user.
This makes sense, but it doesn't seem to take into account implications. For instance, we could have an implication:
```
[W] hole{co1}
===>
[W] hole{co2} {{co1}} :: alpha ~# (beta |> co)
```
When we call `reportWanteds` on this implication, we have the unsolved unrewritten `[W] hole{co1}` to report. Fine. Then we recurse into the implication, and we have a single constraint `[W] hole{co2}` to report, which has been rewritten by `[W] hole{co1}`. This trips up the assertion (we only have rewritten Wanteds to report), even though at an outer level we reported an unrewritten Wanted.
@rae, do you agree that the assertion is wrong?https://gitlab.haskell.org/ghc/ghc/-/issues/21447Confusing GADTSyntax newtype error with invisible kinds2022-10-13T14:34:21Zsheafsam.derbyshire@gmail.comConfusing GADTSyntax newtype error with invisible kindsConsider the following:
```haskell
type N :: TYPE r -> Type
newtype N a where
MkN :: (a -> N a) -> N a
```
This seems fine, right? Except that the user didn't write a forall in the type of `MkN`, so the kind of `a` is defaulted. Maki...Consider the following:
```haskell
type N :: TYPE r -> Type
newtype N a where
MkN :: (a -> N a) -> N a
```
This seems fine, right? Except that the user didn't write a forall in the type of `MkN`, so the kind of `a` is defaulted. Making the kinds explicit, it's as if we wrote:
```haskell
type N :: forall (r :: RuntimeRep). TYPE r -> Type
newtype N @r a where
MkN :: (a -> N a) -> N @LiftedRep a
```
and this isn't allowed: we can't have a newtype which is a genuine GADT, where the type variables in the return kind don't match those in the head of the declaration.
However, the error message is quite confusing:
```
* A newtype constructor must have a return type of form T a1 ... an
MkN :: forall a. (a -> N a) -> N a
* In the definition of data constructor `MkN'
In the newtype declaration for `N'
|
10 | MkN :: (a -> N a) -> N a
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
```9.6.1Finley McIlwaineFinley McIlwainehttps://gitlab.haskell.org/ghc/ghc/-/issues/21473Regression in interaction between type families and equality constraints2022-07-21T02:42:45ZKingoftheHomelessRegression in interaction between type families and equality constraints## Summary
I've encountered a regression in GHC 9.2.2 where a flexible instance requiring `R ~ e ': some_tail` fails to apply even when given the context `R ~ e ': F R`, where `F`, `R` are type families. However, adding the seemingly re...## Summary
I've encountered a regression in GHC 9.2.2 where a flexible instance requiring `R ~ e ': some_tail` fails to apply even when given the context `R ~ e ': F R`, where `F`, `R` are type families. However, adding the seemingly redundant constraint `r ~ R` -- where `r` is an otherwise completely unused polymorphic type variable -- allows the instance to be deduced.
[This issue has broken a library of mine, and I haven't yet found a good workaround while preserving the library's current API.](https://github.com/KingoftheHomeless/in-other-words/issues/18)
## Steps to reproduce
[Minimal reproducer](/uploads/85a907b0e63735a1e8fe96f19767747d/reproducer.hs). The `errors` function is rejected with:
```
• Could not deduce (Foo Int R) arising from a use of ‘Dict’
from the context: R ~ (Int : F R)
```
## Environment:
Reproducer tested on GHC 9.2.2 and errors. Compiles without issue on GHC 9.0.2.9.2.3Richard Eisenbergrae@richarde.devSimon Peyton JonesRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/21479GHC panic2022-06-14T16:14:08ZIcelandjackGHC panicghc-9.2.2, I don't know if this has been fixed
```haskell
{-# Language ConstraintKinds #-}
{-# Language PatternSynonyms #-}
{-# Language ViewPatterns #-}
{-# Language TypeOperators #-}
{-# Language GADTs #-}
{-# Language PolyKinds #-}
...ghc-9.2.2, I don't know if this has been fixed
```haskell
{-# Language ConstraintKinds #-}
{-# Language PatternSynonyms #-}
{-# Language ViewPatterns #-}
{-# Language TypeOperators #-}
{-# Language GADTs #-}
{-# Language PolyKinds #-}
{-# Language KindSignatures #-}
{-# Language ScopedTypeVariables #-}
{-# Language TypeApplications #-}
module GHC.Generics.Explicit where
import Data.Type.Equality
import Data.Kind
import Type.Reflection
import GHC.Generics
pattern IsV1 <- (isV1 -> Just HRefl)
isV1 :: TypeRep rep -> Maybe (V1 :~~: rep)
isV1 = eqTypeRep @(Type -> Type) @(Type -> Type) (typeRep @V1)
```
produces
```
ghci> :r
[1 of 1] Compiling GHC.Generics.Explicit ( src/GHC/Generics/Explicit.hs, interpreted )
ghc: panic! (the 'impossible' happened)
(GHC version 9.2.2:
NoFlexi
k_a46D[tau:1] :: *
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:181:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Tc/Utils/Zonk.hs:1932:18 in ghc:GHC.Tc.Utils.Zonk
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```9.2.3Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/21500TypeInType is marked as deprecated but has no warning on usage.2022-05-05T07:44:30ZTrevis ElserTypeInType is marked as deprecated but has no warning on usage.Per [the user's guide](https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/poly_kinds.html#extension-TypeInType) 'TypeInType' is deprecated. However there does not seem to be any warning associated with using it. If it is truly depre...Per [the user's guide](https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/poly_kinds.html#extension-TypeInType) 'TypeInType' is deprecated. However there does not seem to be any warning associated with using it. If it is truly deprecated then can we get a warning on usage of it?https://gitlab.haskell.org/ghc/ghc/-/issues/21501Confusion around visible type application in pattern synonym pattern2023-02-09T17:22:10ZRichard Eisenbergrae@richarde.devConfusion around visible type application in pattern synonym patternSee also #19847
Sometimes, I like to declare
```hs
import Data.Kind
import Type.Reflection
pattern TypeApp ::
forall {k1} {k2} (f :: k1 -> k2) (result :: k2).
Typeable f =>
forall (arg :: k1).
result ~ f arg =>
TypeRep arg ...See also #19847
Sometimes, I like to declare
```hs
import Data.Kind
import Type.Reflection
pattern TypeApp ::
forall {k1} {k2} (f :: k1 -> k2) (result :: k2).
Typeable f =>
forall (arg :: k1).
result ~ f arg =>
TypeRep arg ->
TypeRep result
pattern TypeApp arg_rep <- App (eqTypeRep (typeRep @f) -> Just HRefl) arg_rep
```
This pattern synonym allows me to match on a `TypeRep` to see whether its an application of some known type constructor, like `List` or `Maybe`.
GHC accepts this declaration, as it should.
But using causes chaos:
```hs
f :: TypeRep a -> String
f (TypeApp @[] rep) = show rep
```
produces
```
Bug.hs:18:4: error:
• No instance for (Typeable f0) arising from a use of ‘TypeApp’
• In the pattern: TypeApp @[] rep
In an equation for ‘f’: f (TypeApp @[] rep) = show rep
|
18 | f (TypeApp @[] rep) = show rep
| ^^^^^^^^^^^^^^^
Bug.hs:18:4: error:
• Could not deduce (k1 ~ *)
from the context: a ~ f0 arg
bound by a pattern with pattern synonym:
TypeApp :: forall {k1} {k2} (f :: k1 -> k2) (result :: k2).
Typeable f =>
forall (arg :: k1).
(result ~ f arg) =>
TypeRep arg -> TypeRep result,
in an equation for ‘f’
at Bug.hs:18:4-18
‘k1’ is a rigid type variable bound by
the type signature for:
f :: forall {k1} (a :: k1). TypeRep a -> String
at Bug.hs:17:1-24
• In the pattern: TypeApp @[] rep
In an equation for ‘f’: f (TypeApp @[] rep) = show rep
• Relevant bindings include
f :: TypeRep a -> String (bound at Bug.hs:18:1)
|
18 | f (TypeApp @[] rep) = show rep
| ^^^^^^^^^^^^^^^
```
I have no clue what GHC is thinking here. Even when I try making `k1` and `k2` *specified* (in parens, not braces) and stating `@Type @Type`, GHC is no better off, producing roughly the same messages.
For the record, this was encountered while I was writing a library that is intended to be useful in the Real World.https://gitlab.haskell.org/ghc/ghc/-/issues/21515Constraint solver regression in 9.22022-12-20T12:54:30ZAndres LöhConstraint solver regression in 9.2## Summary
When porting some generics-sop code from GHC 8.10 to GHC 9.2, I discovered a regression in the type checker.
## Steps to reproduce
Run GHC on the following program:
```haskell
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ...## Summary
When porting some generics-sop code from GHC 8.10 to GHC 9.2, I discovered a regression in the type checker.
## Steps to reproduce
Run GHC on the following program:
```haskell
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module ConstraintTest2 where
import Data.Kind
type family Code a :: [[Type]]
type IsWrappedType a x = Code a ~ '[ '[ x ] ]
type IsProductType a xs = Code a ~ '[ xs ]
type family Head (xs :: [a]) :: a where
Head (x : xs) = x
type ProductCode a = Head (Code a)
type WrappedCode a = Head (Head (Code a))
wrappedTypeTo :: IsWrappedType a x => x -> a
wrappedTypeTo = undefined
to :: SOP (Code a) -> a
to = undefined
data SOP (xss :: [[a]])
type WrappedProduct a = (IsWrappedType a (WrappedCode a), IsProductType (WrappedCode a) (ProductCode (WrappedCode a)))
process :: (SOP '[ xs ] -> a) -> a
process = undefined
-- works with 8.10 and 9.0, fails with 9.2
test :: WrappedProduct a => a
test = process (wrappedTypeTo . to)
```
## Expected behavior
I expect the program to compile, as it does with GHC 8.10 and GHC 9.0. However, with GHC 9.2, I get:
```
/home/andres/trans/ConstraintTest2.hs:37:17: error:
• Could not deduce: Code a ~ '[ '[b0]]
arising from a use of ‘wrappedTypeTo’
from the context: WrappedProduct a
bound by the type signature for:
test :: forall a. WrappedProduct a => a
at /home/andres/trans/ConstraintTest2.hs:36:1-29
The type variable ‘b0’ is ambiguous
• In the first argument of ‘(.)’, namely ‘wrappedTypeTo’
In the first argument of ‘process’, namely ‘(wrappedTypeTo . to)’
In the expression: process (wrappedTypeTo . to)
• Relevant bindings include
test :: a (bound at /home/andres/trans/ConstraintTest2.hs:37:1)
|
37 | test = process (wrappedTypeTo . to)
| ^^^^^^^^^^^^^
/home/andres/trans/ConstraintTest2.hs:37:33: error:
• Could not deduce: Code b0 ~ '[xs0]
from the context: WrappedProduct a
bound by the type signature for:
test :: forall a. WrappedProduct a => a
at /home/andres/trans/ConstraintTest2.hs:36:1-29
Expected: SOP '[xs0] -> b0
Actual: SOP (Code b0) -> b0
The type variables ‘b0’, ‘xs0’ are ambiguous
• In the second argument of ‘(.)’, namely ‘to’
In the first argument of ‘process’, namely ‘(wrappedTypeTo . to)’
In the expression: process (wrappedTypeTo . to)
|
37 | test = process (wrappedTypeTo . to)
| ^^
```
## Environment
* GHC version used: 9.2.29.2.3https://gitlab.haskell.org/ghc/ghc/-/issues/21530GHC 9.4 infinite loop in typechecker2022-11-12T22:54:01ZJaro ReindersGHC 9.4 infinite loop in typechecker## Summary
Compiling the following program with GHC 9.4.1 leads to a infinite loop during type checking:
```haskell
{-# LANGUAGE RankNTypes #-}
module T1 where
f :: (forall a. (Show a, Eq a) => a -> String) -> String
f h = h True
g ...## Summary
Compiling the following program with GHC 9.4.1 leads to a infinite loop during type checking:
```haskell
{-# LANGUAGE RankNTypes #-}
module T1 where
f :: (forall a. (Show a, Eq a) => a -> String) -> String
f h = h True
g :: (forall a. Show a => a -> String) -> String
g = f
```
## Environment
* GHC version used: 9.4.0.202205019.4.1Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/21544GHC 9.4 panic on a representation-polymorphic newtype instance2023-08-28T22:23:31Zsheafsam.derbyshire@gmail.comGHC 9.4 panic on a representation-polymorphic newtype instanceOn GHC 9.4 and HEAD, the following program causes a panic:
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ...On GHC 9.4 and HEAD, the following program causes a panic:
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UnliftedNewtypes #-}
module T21544 where
import Data.Kind
import GHC.Exts
type N :: forall (r :: RuntimeRep) -> TYPE r -> TYPE r
data family N r a
newtype instance N r a = MkN a
foo :: Int# -> N IntRep Int#
foo = MkN
```
```
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.5.20220503:
isUnliftedType
a_aXy :: TYPE r_aXx
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler\GHC\Utils\Panic.hs:182:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler\GHC\Core\Type.hs:2484:7 in ghc:GHC.Core.Type
isUnliftedType, called at compiler\GHC\Core\Opt\Simplify.hs:2900:5 in ghc:GHC.Core.Opt.Simplify
```
The program seems to be OK on GHC 9.2 and below.9.4.1Matthew PickeringMatthew Pickeringhttps://gitlab.haskell.org/ghc/ghc/-/issues/21548Investigate whether we can support simplified and deep subsumption2022-11-08T20:25:53ZMatthew PickeringInvestigate whether we can support simplified and deep subsumptionIn the call today we discussed the [reddit thread](https://www.reddit.com/r/haskell/comments/ujpzx3/was_simplified_subsumption_worth_it_for_industry/) which discussed the [simplified subsumption proposal](https://github.com/ghc-proposals...In the call today we discussed the [reddit thread](https://www.reddit.com/r/haskell/comments/ujpzx3/was_simplified_subsumption_worth_it_for_industry/) which discussed the [simplified subsumption proposal](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0287-simplify-subsumption.rst). And [this Haskell Discourse thread](https://discourse.haskell.org/t/r-haskell-was-simplified-subsumption-worth-it-for-industry-haskell/4486/1)
@simonpj indicated that it might be possible to proceed in a manner similar to let generalisation where there is a predictable/simple subsumption mode (ie simplified subsumption) but also unpredictable/deep subsumption mode (ie, the old behaviour).
This ticket is created to track that idea, which Simon wanted to discuss with @rae.
This is perhaps important for tickets like #208189.2.3Matthew PickeringMatthew Pickeringhttps://gitlab.haskell.org/ghc/ghc/-/issues/21550Regression in resolving quantified constraint from GHC 8.10.7 to GHC 9.0.2/9.2.22022-09-01T16:18:22ZIdentical SnowflakeRegression in resolving quantified constraint from GHC 8.10.7 to GHC 9.0.2/9.2.2The following compiles on GHC 8.10.7, but fails on GHC 9.0.2 and GHC 9.2.2:
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE QuantifiedCo...The following compiles on GHC 8.10.7, but fails on GHC 9.0.2 and GHC 9.2.2:
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
module Main where
import Data.Function
import Data.Kind
import GHC.Generics
import GHC.TypeLits
-- inlined generic-data imports:
from' :: Generic a => a -> Rep a ()
from' = from
geq :: (Generic a, Eq (Rep a ())) => a -> a -> Bool
geq = (==) `on` from'
gcompare :: (Generic a, Ord (Rep a ())) => a -> a -> Ordering
gcompare = compare `on` from'
-- test case:
data A (v :: Symbol -> Type -> Type) a b deriving (Generic,Generic1)
instance (Eq a , (forall w z . Eq z => Eq (v w z)) , Eq b) => Eq (A v a b) where
{-# INLINE (==) #-}
(==) = geq
instance (Ord a , (forall w z . Eq z => Eq (v w z)) , (forall w z . Ord z => Ord (v w z)) , Ord b) => Ord (A v a b) where
{-# INLINE compare #-}
compare = gcompare
main :: IO ()
main = pure ()
```9.2.3ZubinZubinhttps://gitlab.haskell.org/ghc/ghc/-/issues/21581ghc.exe: panic! (the 'impossible' happened) using a data family in GHC 9.0.12022-05-18T11:37:58ZUltimateDude101ghc.exe: panic! (the 'impossible' happened) using a data family in GHC 9.0.1## Summary
Compiling the below program causes the following error:
```
Loaded package environment from C:\Users\Owner\AppData\Roaming\ghc\x86_64-mingw32-9.0.1\environments\default
[1 of 1] Compiling Main ( app\Main.hs, app\...## Summary
Compiling the below program causes the following error:
```
Loaded package environment from C:\Users\Owner\AppData\Roaming\ghc\x86_64-mingw32-9.0.1\environments\default
[1 of 1] Compiling Main ( app\Main.hs, app\Main.o )
ghc : ghc.exe: panic! (the 'impossible' happened)
At line:1 char:1
+ ghc app/Main > cabal-output.txt 2>&1
+ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+ CategoryInfo : NotSpecified: (ghc.exe: panic!...ible' happened):String) [], RemoteException
+ FullyQualifiedErrorId : NativeCommandError
(GHC version 9.0.1:
No skolem info:
[k_ah0[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler\GHC\Utils\Outputable.hs:1230:37 in ghc:GHC.Utils.Outputable
pprPanic, called at compiler\\GHC\\Tc\\Errors.hs:2810:17 in ghc:GHC.Tc.Errors
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```
## Steps to reproduce
Compile the following program:
```
{-# LANGUAGE PolyKinds, RankNTypes, TypeFamilies #-}
module Main where
class TypeLike k where
data ToType :: k -> *
instance TypeLike k => TypeLike (k1 -> k) where
data ToType f = ToType1 (forall x. f x)
```
## Expected behavior
I expect to get an error because the kind of `forall x. f x` should be `k`, not `*`
## Environment
* ghc 9.0.1
Optional:
* Operating System: Windows 10https://gitlab.haskell.org/ghc/ghc/-/issues/21583flatten_args wandered into deeper water than usual2022-09-28T13:09:20Zsfultongflatten_args wandered into deeper water than usual## Summary
GHC panics because of issue in title.
```
[11 of 12] Compiling Telomare.Possible ( src/Telomare/Possible.hs, /home/sfultong/code/stand-in-language/dist-newstyle/build/x86_64-linux/ghc-8.10.7/telomare-0.1.0.0/build/Telomare/Po...## Summary
GHC panics because of issue in title.
```
[11 of 12] Compiling Telomare.Possible ( src/Telomare/Possible.hs, /home/sfultong/code/stand-in-language/dist-newstyle/build/x86_64-linux/ghc-8.10.7/telomare-0.1.0.0/build/Telomare/Possible.o, /home/sfultong/code/stand-in-language/dist-newstyle/build/x86_64-linux/ghc-8.10.7/telomare-0.1.0.0/build/Telomare/Possible.dyn_o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.10.7:
flatten_args wandered into deeper water than usual
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1179:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcFlatten.hs:1029:21 in ghc:TcFlatten
```
## Steps to reproduce
Compile https://github.com/sfultong/stand-in-language/blob/7d844b0271156988dad9f843810ed9e98042c6f8/src/Telomare/Possible.hs
## Expected behavior
No GHC panic.
## Environment
* GHC version used: 8.10.7
Optional:
* Operating System:
* System Architecture:https://gitlab.haskell.org/ghc/ghc/-/issues/21605Qualified names in type signatures2023-01-11T20:49:37ZVladislav ZavialovQualified names in type signaturesHere's what happens when I try to use a qualified name in a type signature:
```haskell
Prelude> x :: Prelude.id Int
<interactive>:2:6: error: parse error on input ‘Prelude.id’
```
This is not very informative: there isn't any obvious o...Here's what happens when I try to use a qualified name in a type signature:
```haskell
Prelude> x :: Prelude.id Int
<interactive>:2:6: error: parse error on input ‘Prelude.id’
```
This is not very informative: there isn't any obvious obstacle to parsing it. I would rather read a message like this:
```
<interactive>:3:6: error:
• ‘Prelude.id’ is a term-level binding
and can not be used at the type level.
```
Besides, we will likely allow such code at some point in the future (as part of the dependent types effort). So I believe that it would be a good idea to do some preparatory work in GHC and extend the parser accordingly.
I propose that we let qualified names like `Prelude.id` pass through the parser and the renamer (assuming the name in scope, otherwise the renamer would complain, of course). Then reject them in the type checker with a more informative message than what we have currently.Rinat Striungislazybonesxp@gmail.comRinat Striungislazybonesxp@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/21650runtimeRepPrimRep panic with a representation-polymorphic newtype2023-08-28T22:23:31Zsheafsam.derbyshire@gmail.comruntimeRepPrimRep panic with a representation-polymorphic newtypeThe following program runs into a panic on HEAD:
```haskell
{-# LANGUAGE DataKinds, DatatypeContexts, MagicHash, UnliftedNewtypes, TypeFamilies #-}
module EtaExpandNewtypeTF where
import Data.Kind
import GHC.Exts
type R :: Type -> Ru...The following program runs into a panic on HEAD:
```haskell
{-# LANGUAGE DataKinds, DatatypeContexts, MagicHash, UnliftedNewtypes, TypeFamilies #-}
module EtaExpandNewtypeTF where
import Data.Kind
import GHC.Exts
type R :: Type -> RuntimeRep
type family R a where
R Float = FloatRep
R Double = DoubleRep
type F :: forall (a :: Type) -> TYPE (R a)
type family F a where
F Float = Float#
F Double = Double#
type C :: Type -> Constraint
class C a where {}
type N :: forall (a :: Type) -> TYPE (R a)
newtype C a => N a = MkN (F a)
foo1 :: C Float => F Float -> N Float
foo1 = MkN
foo2 :: C Double => () -> F Double -> N Double
foo2 _ = MkN
```
```
GHC version 9.5.20220525:
runtimeRepPrimRep
typePrimRep (F Float :: TYPE (R Float))
R Float
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler\GHC\Utils\Panic.hs:182:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler\GHC\Types\RepType.hs:614:5 in ghc:GHC.Types.RepType
runtimeRepPrimRep, called at compiler\GHC\Types\RepType.hs:582:5 in ghc:GHC.Types.RepType
kindPrimRep, called at compiler\GHC\Types\RepType.hs:534:18 in ghc:GHC.Types.RepType
typePrimRep, called at compiler\GHC\Types\RepType.hs:181:22 in ghc:GHC.Types.RepType
isZeroBitTy, called at compiler\GHC\Core\Unfold.hs:617:43 in ghc:GHC.Core.Unfold
```
We also get an error with Core Lint:
```
*** Core Lint errors : in result of Desugar (after optimization) ***
EtaExpandNewtypeTF.hs:25:1: warning:
Binder does not have a fixed runtime representation: ds_dHN :: (F Float :: TYPE
(R Float))
In the RHS of foo1 :: C Float =>
(F Float |> (TYPE (D:R:R[0]))_N)
-> (N Float |> (TYPE (D:R:R[0]))_N)
In the body of lambda with binder $dC_aH8 :: C Float
In the body of lambda with binder ds_dHN :: F Float
Substitution: [TCvSubst
In scope: InScope {}
Type env: []
Co env: []]
```
This seems to be a different issue than #21544, as changing newtype constructors to always inline fixes that bug but doesn't fix this one.https://gitlab.haskell.org/ghc/ghc/-/issues/21667Type inference regression from GHC 8.10.7 to 9.0.2/9.2.32022-06-20T19:03:05ZIdentical SnowflakeType inference regression from GHC 8.10.7 to 9.0.2/9.2.3The following is accepted (with a warning telling the solution to `_`) on GHC 8.10.7, but fails to type check on newer GHCs:
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-...The following is accepted (with a warning telling the solution to `_`) on GHC 8.10.7, but fails to type check on newer GHCs:
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE RankNTypes #-}
module Main where
import GHC.TypeLits
import Data.Functor.Identity
import Data.Functor.Const
import Data.Functor
-- import fluff
type ASetter s t a b = (a -> Identity b) -> s -> Identity t
type Getting r s a = (a -> Const r a) -> s -> Const r s
type Lens s t a b = forall f . Functor f => (a -> f b) -> (s -> f t)
type Traversal s t a b = forall f . Applicative f => (a -> f b) -> (s -> f t)
set :: ASetter s t a b -> b -> s -> t
set = undefined
view :: MonadReader s m => Getting a s a -> m a
view = undefined
class Monad m => MonadReader r (m :: * -> *) | m -> r where
instance MonadReader r ((->) r) where
-- test case
data Item (a :: *) (f :: Symbol -> * -> *)
l :: Lens (Item a f) (Item a' g) (f "1" ()) (g "1" ())
l = undefined
type ExoticTraversal' a y f = Traversal
(Item a f)
(Item a f)
(f y ())
(f y ())
test :: ExoticTraversal' a _ f
test f x = f (view l x) <&> \w -> set l w x
main :: IO ()
main = pure ()
```9.2.4sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/21719Type checking with PartialTypeSignatures is broken2022-08-17T10:21:48ZDanil BerestovType checking with PartialTypeSignatures is broken## Steps to reproduce
```haskell
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE BlockArguments #-}
impor...## Steps to reproduce
```haskell
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE BlockArguments #-}
import Control.Exception
data Foo = Foo
deriving (Show, Exception)
class CanThrow e
qux :: Monad m => (CanThrow Foo => m a) -> m a
qux _ = undefined
class Monad m => MonadCheckedThrow m where
throwChecked :: (Exception e, CanThrow e) => e -> m a
foo :: MonadCheckedThrow m => m Int
foo = do
qux do
_ <- baz
pure 5
where
baz :: (CanThrow Foo, _) => _
baz = throwChecked Foo
```
```
error:
• Could not deduce (CanThrow Foo)
from the context: MonadCheckedThrow m
bound by the type signature for:
foo :: forall (m :: * -> *). MonadCheckedThrow m => m Int
at _
or from: MonadCheckedThrow m1
bound by the inferred type for ‘baz’:
forall (m1 :: * -> *) a. MonadCheckedThrow m1 => m1 a
at _
• When checking that the inferred type
baz :: forall (m :: * -> *) a.
(CanThrow Foo, MonadCheckedThrow m) =>
m a
is as general as its (partial) signature
baz :: forall (m :: * -> *) a. MonadCheckedThrow m => m a
In an equation for ‘foo’:
foo
= do qux
do _ <- baz
....
where
baz :: (CanThrow Foo, _) => _
baz = throwChecked Foo
```
## Expected behavior
GHC must check `bar`'s type.
By the way the following code is checked:
```haskell
baz :: (c ~ CanThrow, c Foo, _) => _
baz = throwChecked Foo
-- and
baz :: (f ~ Foo, CanThrow f, _) => _
baz = throwChecked Foo
-- and even
baz :: _ => CanThrow Foo => _
baz = throwChecked Foo
```
## Environment
* GHC version used: 8.10.7Matthew PickeringMatthew Pickeringhttps://gitlab.haskell.org/ghc/ghc/-/issues/21765`-Wredundant-constraints` false positives in class instance contexts2023-08-31T04:27:45Zyairchu`-Wredundant-constraints` false positives in class instance contexts## Summary
In the following example:
```Haskell
{-# LANGUAGE UndecidableInstances, FlexibleInstances #-}
class Functor f => C f where c :: f Int
instance (Functor f, Applicative f) => C f where c = pure 42
```
Compiling in GHC 9.2.3...## Summary
In the following example:
```Haskell
{-# LANGUAGE UndecidableInstances, FlexibleInstances #-}
class Functor f => C f where c :: f Int
instance (Functor f, Applicative f) => C f where c = pure 42
```
Compiling in GHC 9.2.3 using `-Wredundant-constraints` produces the following warning:
```Haskell
test.hs:5:10: warning: [-Wredundant-constraints]
• Redundant constraint: Functor f
• In the instance declaration for ‘C f’
|
5 | instance (Functor f, Applicative f) => C f where c = pure 42
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
While the constraint intuitively seems redundant, in the case of instance contexts it is in fact necessary, by design, as [described here](https://stackoverflow.com/a/72690345/40916)
## Expected behavior
As in previous GHC versions, like 9.0.2, no warning should be given in this case.9.8.1sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/21806Example in ghc doc for SAKS doesn't work2022-07-29T11:00:01ZGeorgi LyubenovExample in ghc doc for SAKS doesn't workNot sure if this is a bug or a documentation issue, but an example from the [ghc docs on SAKS](https://downloads.haskell.org/ghc/latest/docs/html/users_guide/exts/poly_kinds.html#standalone-kind-signatures-and-declaration-headers) doesn'...Not sure if this is a bug or a documentation issue, but an example from the [ghc docs on SAKS](https://downloads.haskell.org/ghc/latest/docs/html/users_guide/exts/poly_kinds.html#standalone-kind-signatures-and-declaration-headers) doesn't compile:
```haskell
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
import Data.Kind
type GProx4 :: k -> Type
data GProx4 :: w where MkGProx4 :: GProx4 a
```
```sh
[nix-shell:~]$ ghci --version
The Glorious Glasgow Haskell Compilation System, version 9.2.2
[nix-shell:~]$ ghci /tmp/asdf.hs
GHCi, version 9.2.2: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/googleson78/.ghci
[1 of 1] Compiling Main ( /tmp/asdf.hs, interpreted )
/tmp/asdf.hs:10:1: error:
• Couldn't match expected kind ‘w’ with actual kind ‘k -> *’
• In the data type declaration for ‘GProx4’
|
10 | data GProx4 :: w where MkGProx4 :: GProx4 a
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.
>
```sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/21896Panic when checking type family dependency2022-07-26T07:49:55ZGergő ÉrdiPanic when checking type family dependency```
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE DataKinds, TypeFamilies, TypeFamilyDependencies, PolyKinds #-}
module Bug where
data T = Foo | Bar
type family F (ns :: T) (ret :: k) = (r :: k) | r -> ret where
F Foo r = r
F...```
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE DataKinds, TypeFamilies, TypeFamilyDependencies, PolyKinds #-}
module Bug where
data T = Foo | Bar
type family F (ns :: T) (ret :: k) = (r :: k) | r -> ret where
F Foo r = r
F Bar r = r
```
On a GHC as of e2f0094c315746ff15b8d9650cf318f81d8416d7, with sufficient sanity checks (i.e. compiled with `-DDEBUG`), this crashes with:
```
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.5.20220719:
ASSERT failed!
in_scope InScope {r_a9 k_aJ}
tenv [a9 :-> r_a9, aa :-> r_a9, aJ :-> k_aJ]
cenv []
tys [k_aN, r_aa]
cos []
needInScope {k_aN}
Call stack:
CallStack (from HasCallStack):
assertPpr, called at compiler/GHC/Core/TyCo/Subst.hs:645:5 in ghc:GHC.Core.TyCo.Subst
checkValidSubst, called at compiler/GHC/Core/TyCo/Subst.hs:694:17 in ghc:GHC.Core.TyCo.Subst
substTys, called at compiler/GHC/Core/FamInstEnv.hs:568:25 in ghc:GHC.Core.FamInstEnv
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```https://gitlab.haskell.org/ghc/ghc/-/issues/21898Problems disambiguating a record update with pattern synonyms2023-03-30T13:28:39Zsheafsam.derbyshire@gmail.comProblems disambiguating a record update with pattern synonymsThe parent of a pattern synonym record field is the pattern synonym itself, which I think makes sense (a pattern synonym behaves much like a data constructor). However, it seems that the following variant on #21443 causes GHC to trip ove...The parent of a pattern synonym record field is the pattern synonym itself, which I think makes sense (a pattern synonym behaves much like a data constructor). However, it seems that the following variant on #21443 causes GHC to trip over:
```haskell
{-# LANGUAGE DuplicateRecordFields, PatternSynonyms #-}
pattern P :: Int -> Int -> (Int, Int)
pattern P { proj_x, proj_y } = (proj_x, proj_y)
pattern Q1 :: Int -> Int
pattern Q1 { proj_x } = proj_x
pattern Q2 :: Int -> Int
pattern Q2 { proj_y } = proj_y
blah :: (Int, Int) -> (Int, Int)
blah p = p { proj_x = 0, proj_y = 1 }
```
```
error:
* GHC internal error: `T21443b.$sel:proj_x:P' is not in scope during type checking, but it passed the renamer
tcl_env of environment: [auv :-> Identifier[p::(Int,
Int), NotLetBound],
rgF :-> Identifier[blah::(Int, Int)
-> (Int, Int), TopLevelLet {} True]]
* In the expression: p {proj_x = 0, proj_y = 1}
In an equation for `blah': blah p = p {proj_x = 0, proj_y = 1}
|
| blah p = p { proj_x = 0, proj_y = 1 }
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```9.8.1sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/21906FixedRuntimeRep: check type arguments instead of value arguments for Ids with...2023-07-18T12:23:35Zsheafsam.derbyshire@gmail.comFixedRuntimeRep: check type arguments instead of value arguments for Ids with no bindingCurrently, we rule out bad representation-polymorphism in primops (and other `Id`s with no binding) through `tcRemainingValArgs`, which checks that the remaining value arguments all have a fixed `RuntimeRep`.
However, @bgamari points ou...Currently, we rule out bad representation-polymorphism in primops (and other `Id`s with no binding) through `tcRemainingValArgs`, which checks that the remaining value arguments all have a fixed `RuntimeRep`.
However, @bgamari points out in #21868 that we also need to rule out representation-polymorphism in other places that aren't arguments, such as the return `RuntimeRep` `r_rep` of `catch#` or `keepAlive#`:
```haskell
catch# :: forall (r_rep :: RuntimeRep) (r :: TYPE r_rep) w.
(State# RealWorld -> (# State# RealWorld, r #) )
-> (w -> State# RealWorld -> (# State# RealWorld, r #) )
-> State# RealWorld
-> (# State# RealWorld, r #)
keepAlive# :: forall (a_lev :: Levity) (a :: TYPE (BoxedRep lev))
(r_rep :: RuntimeRep) (r :: TYPE r_rep).
a -> State# RealWorld -> (State# RealWorld -> r) -> r
```
Furthermore, it is not enough to rule out representation-polymorphism: #21868 points out that the current implementation of these primops imposes further restrictions on the representation, because the passing of evaluation results may happen via the stack (e.g. in the case of an unregisterised compiler). The current implementation allows non-`Void` `PrimRep`s that are word-sized or smaller. This means that `BoxedRep Lifted`, `BoxedRep Unlifted`, `WordRep`, `Word8Rep`, `AddrRep` for example are all OK, while `FloatRep`, `TupleRep '[]` and `TupleRep '[ IntRep, WordRep ]` are all disallowed. This is a detail of the current implementation of these primops; this limitation could conceivably be lifted (see discussion on #21868).
## Plan
Here's a plan, elaborated with @simonpj and @monoidal:
### Step 1: store concreteness information in `IdDetails`
`Id`s whose type quantifies over `RuntimeRep`s which must be instantiated to concrete `RuntimeRep`s should store this information in their `IdDetails`:
1. For primops, we can replace the "is rep-poly" `Bool` stored in the `PrimOpId` constructor with a collection of type variables and associated `ConcreteTvOrigin`. For example, `catch#` would say that the `RuntimeRep` variable needs to be instantiated to a concrete `RuntimeRep`.
2. For wired-in `Id`s with a compulsory unfolding and representation-polymorphic arguments, add a new constructor to `IdDetails` with this same information.
3. For unboxed tuples and sums, we know ahead of time that the `RuntimeRep` arguments should be concrete (the first half of the type arguments).
4. This leaves representation-polymorphic newtype constructors, for which this strategy won't work because it might be some type other than one of the quantified type variables which is required to be concrete. See [§ The newtype question](#the-newtype-question) below.
### Step 2: create Concrete metavariables when instantiating
When instantiating an `Id` which contains this information, use concrete metavariables instead of `TauTv`s for the appropriately tagged variables.
To be specific, in `tcInstFun.go1`, when we split off some type variables using `tcSplitSomeForAllTyVars`, if `acc` is empty (i.e. we are instantiating at the top-level, not in a nested situation) and the function being applied is an `Id` with no binding, look up which variables must be concrete from the `Id` and pass that information on to `instantiateSigma`, saying to use `newConcreteTyVarX` instead of `newMetaTyVarX` for those variables.
Other than the wrinkle with representation-polymorphic unlifted newtypes, this would **allow us to remove `tcRemainingValArgs`**, as we will be ensuring concreteness right at the source, when the type variables are created. This means we will be able to accept
```haskell
type R :: RuntimeRep
type family R where { R = IntRep }
myId :: forall (a :: TYPE R). a -> a
myId = coerce
```
effectively implementing PHASE 2 of FixedRuntimeRep for primops without having to pay the onerous implementation cost of inserting the correct coercions when eta-expanding.
### Step 3: check concreteness in Core Lint
The above steps attempt to instantiate these "MustBeConcrete" type variables to concrete types. We want to check that this is indeed the case, and that further transformations don't break the invariant. So we should also add a check to Core Lint to ensure that in any application of an `Id` with no binding, the types it requires to be concrete are indeed concrete.
## The newtype question
In [Step 1](#step-1), (4), we alluded to the observation that storing which type variables must be concrete might not be sufficient for representation-polymorphic newtype constructors. For example:
```haskell
type R :: Type -> RuntimeRep
type family R a
type family T :: Type -> TYPE (R a)
type family T a
type N :: forall (a :: Type) -> TYPE (R a)
data N a = MkN (T a)
```
In this case, the type that needs to be concrete is `R a`, which is not a type variable.
### Option 1: store types instead of type variables
We could directly store which types must be concrete, instead of referring to type variables which must be concrete. Then, to adapt the plan from [Step 2](#step-2), in `instantiateSigma` we would:
1. create new meta type variables as usual,
2. apply the obtained substitution to the types that must be concrete,
3. ensure these substituted types are concrete.
Unfortunately it isn't clear what we would do with the evidence.
### Option 2: change the newtype wrapper
We could change the newtype wrapper for `MkN` to be something like:
```haskell
MkN :: forall {conc :: RuntimeRep}. forall (a :: TYPE) -> R a ~# conc => T a -> N a
```
That is, we add an extra inferred type variable which must be concrete, and add an equality predicate between that concrete type variable and the representation of the type stored inside the newtype. We can then make use of this coercion in the compulsory unfolding of `MkN`. (The type variable `conc` is inferred and comes first, so as to not intefere with visible type applications.)
This brings us back to the case of type variables, which we can handle as in [Step 2](#step-2).
It isn't clear how much extra work this would be, as now we have a newtype worker, one of whose arguments is a coercion. This seems OK, as we already allow e.g. a newtype with a stupid theta. I think it would mean adding an `eq_pred` to the `Haskell98` datacon declaration however, and I don't know what knock-on consequences that might have.9.8.1sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/21909UndecidableSuperClasses fails to terminate when inferring type in where-clause2023-03-09T14:52:54ZBrandon ChinnUndecidableSuperClasses fails to terminate when inferring type in where-clause## Summary
When defining a class with a recursive constraint on an associated type family, functions using that constraint fail to type check when inferring type in a where clause.
Related to:
* https://gitlab.haskell.org/ghc/ghc/-/iss...## Summary
When defining a class with a recursive constraint on an associated type family, functions using that constraint fail to type check when inferring type in a where clause.
Related to:
* https://gitlab.haskell.org/ghc/ghc/-/issues/20836
* https://gitlab.haskell.org/ghc/ghc/-/issues/19627
## Steps to reproduce
The following fails on all GHC versions I've tested, 8.2 to 9.4.1-rc1.
```hs
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableSuperClasses #-}
import Data.Kind
class (Monad m, MyMonad (Inner m)) => MyMonad m where
type Inner m :: Type -> Type
foo :: m Int
works :: MyMonad m => m String
works = show <$> ((+ 1) <$> foo)
fails :: MyMonad m => m String
fails = show <$> fooPlusOne
where
fooPlusOne = (+ 1) <$> foo
alsoFails :: MyMonad m => m String
alsoFails =
let fooPlusOne = (+ 1) <$> foo
in show <$> fooPlusOne
```
This errors with:
```
• solveWanteds: too many iterations (limit = 4)
Unsolved: WC {wc_simple =
[D] _ {0}:: Monad f0 (CDictCan)
[D] _ {0}:: Monad (Inner f0) (CDictCan)
[D] _ {0}:: Monad (Inner (Inner f0)) (CDictCan)
[D] _ {0}:: Monad (Inner (Inner (Inner f0))) (CDictCan)
[D] _ {0}:: Applicative f0 (CDictCan)
[D] _ {0}:: Applicative (Inner f0) (CDictCan)
[D] _ {0}:: Applicative (Inner (Inner f0)) (CDictCan)
[D] _ {0}:: Applicative (Inner (Inner (Inner f0))) (CDictCan)
[WD] $dFunctor_aJ3 {0}:: Functor f0 (CDictCan)
[D] _ {0}:: Functor (Inner f0) (CDictCan)
[D] _ {0}:: Functor (Inner (Inner f0)) (CDictCan)
[D] _ {0}:: Functor (Inner (Inner (Inner f0))) (CDictCan)
[WD] $dMyMonad_aJM {0}:: MyMonad f0 (CDictCan)
[D] _ {0}:: MyMonad (Inner f0) (CDictCan)
[D] _ {0}:: MyMonad (Inner (Inner f0)) (CDictCan)
[D] _ {0}:: MyMonad (Inner (Inner (Inner f0))) (CDictCan)
[D] _ {0}:: MyMonad
(Inner (Inner (Inner (Inner f0)))) (CDictCan(psc))}
Set limit with -fconstraint-solver-iterations=n; n=0 for no limit
```
At least GHC 9.4.1-rc1 gives a slightly better error message in addition to `too many iterations`:
```
• Could not deduce (Monad
(Inner (Inner (Inner (Inner (Inner m))))))
arising from a superclass required to satisfy ‘MyMonad
(Inner (Inner (Inner (Inner (Inner m)))))’,
arising from a superclass required to satisfy ‘MyMonad
(Inner (Inner (Inner (Inner m))))’,
arising from a superclass required to satisfy ‘MyMonad
(Inner (Inner (Inner m)))’,
arising from a superclass required to satisfy ‘MyMonad
(Inner (Inner m))’,
arising from a superclass required to satisfy ‘MyMonad (Inner m)’,
arising from a superclass required to satisfy ‘MyMonad m’,
arising from a use of ‘foo’
```
## Expected behavior
I know `-XUndecidableSuperClasses` always carries a risk of non-termination. Is this one of those cases that's known to just not work? Or should we try to make this work?
At the very least, I don't see any other issues around this simple example of just moving a thing into a where clause, so this at least provides a locus for discussion. It's also workaround-able by explicitly typing the helper function.
## Environment
* GHC version used: tested all GHC versions from 8.2 to 9.4.1-rc1
Optional:
* Operating System:
* System Architecture:https://gitlab.haskell.org/ghc/ghc/-/issues/21995-Wunused-type-patterns warns on used type variables2023-05-26T07:36:09ZLas Safin-Wunused-type-patterns warns on used type variables## Summary
```haskell
import Data.Kind (Type)
type family UnApply (fx :: Type) :: Type -> Type where
forall (f :: Type -> Type) (x :: Type).
UnApply (f x) = f -- warns about unused `x`
```
```
[1 of 1] Compiling Main ...## Summary
```haskell
import Data.Kind (Type)
type family UnApply (fx :: Type) :: Type -> Type where
forall (f :: Type -> Type) (x :: Type).
UnApply (f x) = f -- warns about unused `x`
```
```
[1 of 1] Compiling Main ( Test.hs, interpreted )
Test.hs:4:31: warning: [-Wunused-type-patterns]
Defined but not used on the right hand side: type variable ‘x’
|
4 | forall (f :: Type -> Type) (x :: Type).
| ^
```
If a type variable is *needed* on the LHS, yet not used on the RHS,
GHC will warn with -Wunused-type-patterns, even if removing that variable or
replacing it with `_` will give an error.
## Steps to reproduce
Compile above example with `-Wunused-type-patterns`.
## Expected behavior
It should not give a warning.
## Environment
* GHC version used: 9.2.4sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/22065Core Lint error from PartialTypeSignatures2022-08-18T20:59:40ZIcelandjackCore Lint error from PartialTypeSignaturesRunning on ghc-9.2.3, produces a Core Lint error:
```haskell
{-# Options_GHC -dcore-lint #-}
{-# Language PartialTypeSignatures #-}
data Foo where
Apply :: (x -> Int) -> x -> Foo
foo :: Foo
foo = Apply f x :: forall a. _ where
f ...Running on ghc-9.2.3, produces a Core Lint error:
```haskell
{-# Options_GHC -dcore-lint #-}
{-# Language PartialTypeSignatures #-}
data Foo where
Apply :: (x -> Int) -> x -> Foo
foo :: Foo
foo = Apply f x :: forall a. _ where
f :: [_] -> Int
f = length @[] @_
x :: [_]
x = mempty @[_]
```
```
ghci> :load ~/hs/5613.hs
[1 of 1] Compiling Main ( /home/baldur/hs/5613.hs, interpreted )
*** Core Lint errors : in result of Desugar (before optimization) ***
/home/baldur/hs/5613.hs:8:20: warning:
The type variable @k_a9Dn[sk:1] is out of scope
In the RHS of foo :: Foo
In the body of letrec with binders x_a9sr :: forall {w}. [w]
In the body of letrec with binders f_a9sq :: forall {w}. [w] -> Int
In the body of lambda with binder a_a9Dz :: k_a9Dn[sk:1]
Substitution: [TCvSubst
In scope: InScope {}
Type env: []
Co env: []]
*** Offending Program ***
Rec {
$tcFoo :: TyCon
[LclIdX]
$tcFoo
= TyCon
13795410111426859749##
2910294326838708211##
$trModule
(TrNameS "Foo"#)
0#
krep$*
$tc'Apply :: TyCon
[LclIdX]
$tc'Apply
= TyCon
16548517680761376676##
14341609333725595319##
$trModule
(TrNameS "'Apply"#)
1#
$krep_a9DG
$krep_a9DI [InlPrag=[~]] :: KindRep
[LclId]
$krep_a9DI = $WKindRepVar (I# 0#)
$krep_a9DH [InlPrag=[~]] :: KindRep
[LclId]
$krep_a9DH = KindRepFun $krep_a9DI $krep_a9DJ
$krep_a9DK [InlPrag=[~]] :: KindRep
[LclId]
$krep_a9DK = KindRepFun $krep_a9DI $krep_a9DL
$krep_a9DG [InlPrag=[~]] :: KindRep
[LclId]
$krep_a9DG = KindRepFun $krep_a9DH $krep_a9DK
$krep_a9DJ [InlPrag=[~]] :: KindRep
[LclId]
$krep_a9DJ = KindRepTyConApp $tcInt ([] @KindRep)
$krep_a9DL [InlPrag=[~]] :: KindRep
[LclId]
$krep_a9DL = KindRepTyConApp $tcFoo ([] @KindRep)
$trModule :: Module
[LclIdX]
$trModule
= Module (TrNameS "plutarch-core-0.1.0-inplace"#) (TrNameS "Main"#)
foo :: Foo
[LclIdX]
foo
= letrec {
x_a9sr :: forall {w}. [w]
[LclId]
x_a9sr
= \ (@w_a9CP) ->
let {
$dMonoid_a9CV :: Monoid [w_a9CP]
[LclId]
$dMonoid_a9CV = $fMonoid[] @w_a9CP } in
letrec {
x_a9CR :: [w_a9CP]
[LclId]
x_a9CR = break<0>() mempty @[w_a9CP] $dMonoid_a9CV; } in
x_a9CR; } in
letrec {
f_a9sq :: forall {w}. [w] -> Int
[LclId]
f_a9sq
= \ (@w_a9D6) ->
let {
$dFoldable_a9De :: Foldable []
[LclId]
$dFoldable_a9De = $fFoldable[] } in
letrec {
f_a9D8 :: [w_a9D6] -> Int
[LclId]
f_a9D8 = break<1>() length @[] $dFoldable_a9De @w_a9D6; } in
f_a9D8; } in
break<2>(x_a9sr,f_a9sq)
(\ (@(a_a9Dz :: k_a9Dn[sk:1])) ->
(\ (@k_a9Dn) (@(a_a9Do :: k_a9Dn)) ->
(\ (@x_X0) (ds_d9DO :: x_X0 -> Int) (ds_d9DP :: x_X0) ->
Apply @x_X0 ds_d9DO ds_d9DP)
@[Any @Type] (f_a9sq @(Any @Type)) (x_a9sr @(Any @Type)))
@(Any @Type) @(Any @(Any @Type)))
@(Any @k_a9Dn[sk:1])
end Rec }
*** End of Offense ***
<no location info>: error:
Compilation had errors
*** Exception: ExitFailure 1
ghci>
```https://gitlab.haskell.org/ghc/ghc/-/issues/22135Type family injectivity annotation is rejected with type variable rhs, even o...2022-09-08T12:32:47ZGergő ÉrdiType family injectivity annotation is rejected with type variable rhs, even on non-endomorphismIn [*Injective Type Families for Haskell*](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/injective-type-families-acm.pdf), the following explanation is given for rejecting bare type variables on RHS:
> ```
> type ...In [*Injective Type Families for Haskell*](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/injective-type-families-acm.pdf), the following explanation is given for rejecting bare type variables on RHS:
> ```
> type family W1 a = r | r -> a
> type instance W1 [a] = a
> ```
>
> To a mathematician this function certainly looks injective. But,
> surprisingly, it does not satisfy Definition 1! Here is a counterexample. Clearly we do have a proof of `(W1 [W1 Int ] ∼
> W1 Int)`, simply by instantiating the type instance with `[a |-> W1 Int]`. But if `W1` was injective in the sense of Definition 1, we could derive a proof of `[W1 Int ] ∼ Int`, and that is plainly false!
>
> Similarly:
>
> ```
> type family W2 a = r | r -> a
> type instance W2 [a] = W2 a
> ```
>
> Again `W2` looks injective. But we can prove `W2 [Int] ∼ W2 Int`,
> simply by instantiating the type instance; then by Definition 1, we
> could then conclude `[Int] ∼ Int`, which is plainly false. So neither
> `W1` nor `W2` are injective, according to our definition. Note that the
> partiality of `W1` and `W2` is critical for the failure case to occur.
In addition to exploiting partiality, the first example also requires `W1` to be an endomorphism, and the second one depends on `[]` being an endomorphism.
So why is the following example still rejected, where the type family is not an endomorphism and not recursive; in fact, even total?
```
newtype Wrapper = Wrap Type
type family Unwrap (x :: Wrapper) = (r :: Type) | r -> x where
Unwrap (Wrap a) = a
```https://gitlab.haskell.org/ghc/ghc/-/issues/22141GHC-9.4 accepts "data" in kinds without DataKinds2023-11-18T13:08:29ZOleg GrenrusGHC-9.4 accepts "data" in kinds without DataKinds```haskell
import GHC.TypeLits (Nat)
import Data.Kind (Type)
data Vector :: Nat -> Type -> Type where
```
is accepted by GHC-9.4 with just `-XHaskell2010 -XGADTSyntax -XKindSignatures`. GHC-9.2 and older require `DataKinds`. I cannot f...```haskell
import GHC.TypeLits (Nat)
import Data.Kind (Type)
data Vector :: Nat -> Type -> Type where
```
is accepted by GHC-9.4 with just `-XHaskell2010 -XGADTSyntax -XKindSignatures`. GHC-9.2 and older require `DataKinds`. I cannot find anything in release notes justifying this change.
If it's intentional, please amend release notes.
--------------------------
Here is a specification for what `-XDataKinds` allows, or doesn't. First, some definitions:
* A user-written type (i.e. part of the source text of a program) is in a **kind context** if it follows a "::" in:
* A standalone kind signature (e.g. `type T :: Nat -> Type`)
* A kind signature in a type (e.g. `forall (a :: Nat -> Type). blah`, `type F = G :: Nat -> Type`, etc.)
* A result kind signature in a type declaration (e.g. `data T a :: Nat -> Type where ...`, `type family Fam :: Nat -> Type`, etc.)
* All other contexts where types can appear are referred to as **type contexts**.
* The **kind type constructors** are (see `GHC.Core.TyCon.isKindTyCon`):
* `TYPE` and `Type`
* `CONSTRAINT` and `Constraint`
* `LiftedRep`
* `RuntimeRep`, `Levity`, and their data constructors
* `Multiplicity` and its data construtors
* `VecCount`, `VecElem`, and their data constructors
* A **`type data` type constructor** is defined using the `TypeData` extension, such as the `T` in `type data T = A | B`.
* The following are rejected in type contexts unless `-XDataKinds` is enabled:
* Promoted data constructors (e.g., `'Just`), except for those data constructors listed under "kind type constructors"
* Promoted list or tuple syntax (e.g., `'[Int, Bool]` or `'(Int, Bool)`)
* Type-level literals (e.g., `42`, `"hello"`, or `'a'` at the type level)
* The following are rejected in kind contexts unless `-XDataKinds` is enabled:
* Everything that is rejected in a type context.
* Any type constructor that is not a kind type constructor or a `type data` type constructor (e.g., `Maybe`, `[]`, `Char`, `Nat`, `Symbol`, etc.)
Note that this includes rejecting occurrences of non-kind type construtors in type synomym (or type family) applications, even it the expansion would be legal. For example:
```hs
type T a = Type
f :: forall (x :: T Int). blah
```
Here the `Int` in `T Int` is rejected even though the expansion is just `Type`. This is consistent with, for example, rejecting `T (forall a. a->a)` without `-XImpredicativeTypes`.
This check only occurs in kind contexts. It is always permissible to mention type synonyms in a type context without enabling `-XDataKinds`, even if the type synonym expands to something that would otherwise require `-XDataKinds`.https://gitlab.haskell.org/ghc/ghc/-/issues/22147GHC fails to infer types of certain valid mutually recursive bindings2022-09-06T14:58:40ZJaro ReindersGHC fails to infer types of certain valid mutually recursive bindings## Summary
[User TophatEndermite on Reddit](https://reddit.com/r/haskell/comments/x2xp07/monthly_hask_anything_september_2022/imxz6cb/) posted the following program and asked why GHC can't infer its type:
```haskell
f = g 5 + g "hi"
g ...## Summary
[User TophatEndermite on Reddit](https://reddit.com/r/haskell/comments/x2xp07/monthly_hask_anything_september_2022/imxz6cb/) posted the following program and asked why GHC can't infer its type:
```haskell
f = g 5 + g "hi"
g x = f * 0
```
This produces the following error:
```
T.hs:3:7: error:
• No instance for (Num String) arising from the literal ‘5’
• In the first argument of ‘g’, namely ‘5’
In the first argument of ‘(+)’, namely ‘g 5’
In the expression: g 5 + g "hi"
|
3 | f = g 5 + g "hi"
| ^
```
But it should be quite easy to see that these bindings can be given sensible types:
```haskell
f :: Integer
g :: a -> Integer
```
I thought the monomorphism restriction could be causing the inference failure, but turning it off doesn't help.
I also thought the `Num` constraint could be causing the failure, but even this program without constraints fails to be inferred by GHC:
```haskell
plusInt :: Int -> Int -> Int
plusInt = (+)
timesInt :: Int -> Int -> Int
timesInt = (*)
zero :: Int
zero = 0
five :: Int
five = 5
f = plusInt (g five) (g "hi")
g x = timesInt f zero
```
Why can't GHC infer the types of `f` and `g`?
## Environment
* GHC version used: 9.2.4sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/22151Incorrect constraint warnings from ghc 9.2.42023-08-30T12:18:01ZErik de Castro LopoIncorrect constraint warnings from ghc 9.2.4## Summary
With the constraint, I get a redundant constraint warning and without it, i get a missing constraint warning.
## Steps to reproduce
Minimal reproduction case [redundant-constraint.tgz](/uploads/608384f5071230405e417a3605c09...## Summary
With the constraint, I get a redundant constraint warning and without it, i get a missing constraint warning.
## Steps to reproduce
Minimal reproduction case [redundant-constraint.tgz](/uploads/608384f5071230405e417a3605c095a8/redundant-constraint.tgz)
WIth the code in the tarball I get:
```
• Redundant constraints: (Applicative m, Monad m)
• In the instance declaration for ‘ReportSchemaErrors m’
```
If I remove those constraints I get:
```
• Could not deduce (Applicative m)
• Could not deduce (Monad m)
```
The constraint cannot be both redundant and required.
If the `class` declaration is in the same file as the instance decalration its fine.
## Expected behavior
After removing the redundant constraints, there should be no warning.
## Environment
* GHC version used: 9.2.4
Optional:
* Operating System: Linux
* System Architecture: x86_64sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/22171GHC 9.2.4 regression: unable to compile test application that worked in 9.2.32022-11-08T07:43:06ZDoug BurkeGHC 9.2.4 regression: unable to compile test application that worked in 9.2.3## Summary
Unable to compile the test-rdfproof executable from swish with GHC 9.2.4 as it appears to just hang. I have built this with many previous versions, including GHC 9.2.3.
I originally reported it to [GHC devs](https://mail.has...## Summary
Unable to compile the test-rdfproof executable from swish with GHC 9.2.4 as it appears to just hang. I have built this with many previous versions, including GHC 9.2.3.
I originally reported it to [GHC devs](https://mail.haskell.org/pipermail/ghc-devs/2022-September/020922.html)
## Steps to reproduce
Unfortunately this is an involved process as I have no idea
- what the problem is
- how to just compile the test executable
### Initial diagnosis by Oleg
Before providing the basic reproduction steps (copied from the email above), @phadej provided [some useful compilation info](https://mail.haskell.org/pipermail/ghc-devs/2022-September/020927.html) which I report below
```
I quickly tried with with {-# OPTIONS_GHC -ddump-timings
-ddump-simpl-trace -ddump-to-file #-} in RDFProofTest.hs and at some
point simplifier does nothing. The simpl-trace file doesn't grow. The
GHC just seems to spin.
After that
- I checked out the `ghc-9.2.4-release` tag,
- built it --flavour=default+profiled_ghc+no_dynamic_ghc
- built the swish using cabal pointing to GHC used (on my machine: cabal
build -w /code/ghc/_build_ghc-9.2/stage1/bin/ghc test-rdfproof -v3)
- copy pasted the command cabal used to execute ghc, which is long, and
added +RTS -xc -RTS there
After that, if I ^C when GHC seems to be spinning, the stack trace is
consistently the same:
^C*** Exception (reporting due to +RTS -xc): (THUNK_STATIC), stack trace:
GHC.Core.Opt.Pipeline.CallArity,
called from GHC.Driver.Main.Core2Core,
called from GHC.Driver.Main.hscSimplify',
called from GHC.Driver.Main.finish,
called from GHC.Driver.Main.hscIncrementalCompile,
called from GHC.Driver.Make.upsweep_mod.compile_it,
called from GHC.Driver.Make.upsweep_mod,
called from GHC.Driver.Make.upsweep.upsweep',
called from GHC.Driver.Make.upsweep,
called from GHC.Driver.Make.withDeferredDiagnostics,
called from GHC.Driver.Make.load'.checkHowMuch,
called from GHC.Driver.Make.load',
called from GHC.Driver.Make.load,
called from GHC.withCleanupSession,
called from GHC.runGhc,
called from GHC.defaultErrorHandler
Hopefully this illustrates how to reproduce with your own GHC.
I also tried with GHC-9.4.1 (using --allow-newer=base) and GHC panics:
[ 6 of 55] Compiling Swish.GraphMatch
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.4.1:
funResultTy
GenLabelMap lb_adrG LabelIndex
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:182:37 in
ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Core/Type.hs:1334:49 in
ghc:GHC.Core.Type
GHC-9.4.2 panics in the same way.
Maybe these failures are related?
- Oleg
```
### Download the code
I am on a linux machine (ubuntu 22.04) and have seen this with builds
either with stack or nix.
```
% git clone https://gitlab.com/dburke/swish temp
% cd temp
% git rev-parse HEAD
09c92e0fbbea9be86cac5c8e273e1d5915a9eeae
```
Added to get the timings, but it's not strictly necessary:
```
% sed -i -e "s/-Wall /-Wall -ddump-timings /" swish.cabal
```
### building with stack
If you try with `--resolver lts-19.22` (ghc 9.0.2) then it works. With GHC 9.2.4 it fails:
```
% stack test --resolver nightly-2022-09-05 :test-rdfproof
...
*** Parser [Main]:
Parser [Main]: alloc=24346008 time=8.730
*** Renamer/typechecker [Main]:
Renamer/typechecker [Main]: alloc=58415776 time=44.077
*** Desugar [Main]:
Desugar [Main]: alloc=22148416 time=15.693
*** Simplifier [Main]:
Simplifier [Main]: alloc=651048904 time=530.123
*** Specialise [Main]:
Specialise [Main]: alloc=44412080 time=31.885
*** Float out(FOS {Lam = Just 0,
Consts = True,
OverSatApps = False}) [Main]:
Float out(FOS {Lam = Just 0, Consts = True, OverSatApps = False})
[Main]: alloc=207753368 time=259.238
*** Simplifier [Main]:
Simplifier [Main]: alloc=599788216 time=548.107
*** Simplifier [Main]:
Simplifier [Main]: alloc=562910904 time=474.847
*** Simplifier [Main]:
Simplifier [Main]: alloc=725093584 time=643.255
Float inwards [Main]: alloc=23720 time=0.011
Called arity analysis [Main]: alloc=25856 time=0.012
*** Float inwards [Main]:
*** Called arity analysis [Main]:
*** Simplifier [Main]:
```
At this point it just makes my laptop fan spin faster wit h one of my
CPUs pegged at 100%, but it never seems to print anything more.
### building with nix
This works
```
% nix-shell --argstr compiler ghc923
% cabal test test-rdfproof
```
With 9.2.4 you get similar to above (the screen messages don't quite agree):
```
% nix-shell --argstr compiler ghc924
cabal test test-rdfproof
Warning: The package list for 'hackage.haskell.org' is 20 days old.
Run 'cabal update' to get the latest list of available packages.
Resolving dependencies...
Build profile: -w ghc-9.2.4 -O1
In order, the following will be built (use -v for more details):
- swish-0.10.2.0 (test:test-rdfproof) (first run)
Preprocessing test suite 'test-rdfproof' for swish-0.10.2.0..
Building test suite 'test-rdfproof' for swish-0.10.2.0..
*** initializing unit database:
initializing unit database: alloc=7389248 time=4.462
*** initializing unit database:
initializing unit database: alloc=4001312 time=11.664
*** Chasing dependencies:
*** systool:cpp:
systool:cpp: alloc=319464 time=0.481
Chasing dependencies: alloc=12861208 time=6.331
[2 of 2] Compiling Main ( tests/RDFProofTest.hs,
/home/dburke/rdf/temp/dist-newstyle/build/x86_64-linux/ghc-9.2.4/swish-0.10.2.0/t/test-rdfproof/build/test-rdfproof/test-rdfproof-tmp/Main.o
)
*** Parser [Main]:
Parser [Main]: alloc=25236056 time=23.982
*** Renamer/typechecker [Main]:
Renamer/typechecker [Main]: alloc=101830968 time=97.529
*** Desugar [Main]:
Desugar [Main]: alloc=24617072 time=19.187
*** Simplifier [Main]:
Simplifier [Main]: alloc=665051592 time=558.078
*** Specialise [Main]:
Specialise [Main]: alloc=44894576 time=30.341
*** Float out(FOS {Lam = Just 0,
Consts = True,
OverSatApps = False}) [Main]:
Float out(FOS {Lam = Just 0, Consts = True, OverSatApps = False})
[Main]: alloc=208060752 time=245.458
*** Simplifier [Main]:
Simplifier [Main]: alloc=602721856 time=555.073
*** Simplifier [Main]:
Simplifier [Main]: alloc=563887832 time=529.865
*** Simplifier [Main]:
Simplifier [Main]: alloc=727381840 time=606.367
*** Float inwards [Main]:
Float inwards [Main]: alloc=23720 time=0.012
*** Called arity analysis [Main]:
Called arity analysis [Main]: alloc=25848 time=0.012
*** Simplifier [Main]:
```
and here it hangs.
## Expected behavior
To compile the program.
## Environment
* GHC version used: 9.2.4
Optional:
* Operating System: linux
* System Architecture: x86_64-linux9.2.5Matthew PickeringMatthew Pickering