GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:12:57Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/15370Typed hole panic on GHC 8.6 (tcTyVarDetails)2019-07-07T18:12:57ZRyan ScottTyped hole panic on GHC 8.6 (tcTyVarDetails)The following program panics on GHC 8.6 and HEAD:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperat...The following program panics on GHC 8.6 and HEAD:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
import Data.Type.Equality
import Data.Void
data family Sing :: forall k. k -> Type
data (~>) :: Type -> Type -> Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }
mkRefl :: n :~: j
mkRefl = Refl
right :: forall (r :: (x :~: y) ~> z).
Sing r -> ()
right no =
case mkRefl @x @y of
Refl -> applySing no _
```
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.6.0.20180627 for x86_64-unknown-linux):
tcTyVarDetails
co_a1BG :: y_a1Bz[sk:1] ~# x_a1By[sk:1]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
pprPanic, called at compiler/basicTypes/Var.hs:497:22 in ghc:Var
```
On GHC 8.4, this simply errors:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:23:10: error:
• Couldn't match type ‘n’ with ‘j’
‘n’ is a rigid type variable bound by
the type signature for:
mkRefl :: forall k1 (n :: k1) (j :: k1). n :~: j
at Bug.hs:22:1-17
‘j’ is a rigid type variable bound by
the type signature for:
mkRefl :: forall k1 (n :: k1) (j :: k1). n :~: j
at Bug.hs:22:1-17
Expected type: n :~: j
Actual type: n :~: n
• In the expression: Refl
In an equation for ‘mkRefl’: mkRefl = Refl
• Relevant bindings include
mkRefl :: n :~: j (bound at Bug.hs:23:1)
|
23 | mkRefl = Refl
| ^^^^
Bug.hs:29:13: error:
• Couldn't match type ‘Sing (Apply r t0)’ with ‘()’
Expected type: ()
Actual type: Sing (Apply r t0)
• In the expression: applySing no _
In a case alternative: Refl -> applySing no _
In the expression: case mkRefl @x @y of { Refl -> applySing no _ }
• Relevant bindings include
no :: Sing r (bound at Bug.hs:27:7)
right :: Sing r -> () (bound at Bug.hs:27:1)
|
29 | Refl -> applySing no _
| ^^^^^^^^^^^^^^
Bug.hs:29:26: error:
• Found hole: _ :: Sing t0
Where: ‘t0’ is an ambiguous type variable
‘y’, ‘x’, ‘k’ are rigid type variables bound by
the type signature for:
right :: forall k1 (x1 :: k1) (y1 :: k1) z (r :: (x1 :~: y1) ~> z).
Sing r -> ()
at Bug.hs:(25,1)-(26,21)
• In the second argument of ‘applySing’, namely ‘_’
In the expression: applySing no _
In a case alternative: Refl -> applySing no _
• Relevant bindings include
no :: Sing r (bound at Bug.hs:27:7)
right :: Sing r -> () (bound at Bug.hs:27:1)
Valid substitutions include
undefined :: forall (a :: TYPE r).
GHC.Stack.Types.HasCallStack =>
a
(imported from ‘Prelude’ at Bug.hs:7:8-10
(and originally defined in ‘GHC.Err’))
|
29 | Refl -> applySing no _
| ^
```
Note that this is distinct from #15142, as this is still reproducible on HEAD, even after commit 030211d21207dabb7a4bf21cc9af6fa5eb066db1.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.4.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Typed hole panic on GHC 8.6 (tcTyVarDetails)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeInType,","TypedHoles"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program panics on GHC 8.6 and HEAD:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeApplications #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\nimport Data.Void\r\n\r\ndata family Sing :: forall k. k -> Type\r\n\r\ndata (~>) :: Type -> Type -> Type\r\ninfixr 0 ~>\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\n\r\nnewtype instance Sing (f :: k1 ~> k2) =\r\n SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }\r\n\r\nmkRefl :: n :~: j\r\nmkRefl = Refl\r\n\r\nright :: forall (r :: (x :~: y) ~> z).\r\n Sing r -> ()\r\nright no =\r\n case mkRefl @x @y of\r\n Refl -> applySing no _\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.6.0.20180627 for x86_64-unknown-linux):\r\n tcTyVarDetails\r\n co_a1BG :: y_a1Bz[sk:1] ~# x_a1By[sk:1]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable\r\n pprPanic, called at compiler/basicTypes/Var.hs:497:22 in ghc:Var\r\n}}}\r\n\r\nOn GHC 8.4, this simply errors:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs \r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:23:10: error:\r\n • Couldn't match type ‘n’ with ‘j’\r\n ‘n’ is a rigid type variable bound by\r\n the type signature for:\r\n mkRefl :: forall k1 (n :: k1) (j :: k1). n :~: j\r\n at Bug.hs:22:1-17\r\n ‘j’ is a rigid type variable bound by\r\n the type signature for:\r\n mkRefl :: forall k1 (n :: k1) (j :: k1). n :~: j\r\n at Bug.hs:22:1-17\r\n Expected type: n :~: j\r\n Actual type: n :~: n\r\n • In the expression: Refl\r\n In an equation for ‘mkRefl’: mkRefl = Refl\r\n • Relevant bindings include\r\n mkRefl :: n :~: j (bound at Bug.hs:23:1)\r\n |\r\n23 | mkRefl = Refl\r\n | ^^^^\r\n\r\nBug.hs:29:13: error:\r\n • Couldn't match type ‘Sing (Apply r t0)’ with ‘()’\r\n Expected type: ()\r\n Actual type: Sing (Apply r t0)\r\n • In the expression: applySing no _\r\n In a case alternative: Refl -> applySing no _\r\n In the expression: case mkRefl @x @y of { Refl -> applySing no _ }\r\n • Relevant bindings include\r\n no :: Sing r (bound at Bug.hs:27:7)\r\n right :: Sing r -> () (bound at Bug.hs:27:1)\r\n |\r\n29 | Refl -> applySing no _\r\n | ^^^^^^^^^^^^^^\r\n\r\nBug.hs:29:26: error:\r\n • Found hole: _ :: Sing t0\r\n Where: ‘t0’ is an ambiguous type variable\r\n ‘y’, ‘x’, ‘k’ are rigid type variables bound by\r\n the type signature for:\r\n right :: forall k1 (x1 :: k1) (y1 :: k1) z (r :: (x1 :~: y1) ~> z).\r\n Sing r -> ()\r\n at Bug.hs:(25,1)-(26,21)\r\n • In the second argument of ‘applySing’, namely ‘_’\r\n In the expression: applySing no _\r\n In a case alternative: Refl -> applySing no _\r\n • Relevant bindings include\r\n no :: Sing r (bound at Bug.hs:27:7)\r\n right :: Sing r -> () (bound at Bug.hs:27:1)\r\n Valid substitutions include\r\n undefined :: forall (a :: TYPE r).\r\n GHC.Stack.Types.HasCallStack =>\r\n a\r\n (imported from ‘Prelude’ at Bug.hs:7:8-10\r\n (and originally defined in ‘GHC.Err’))\r\n |\r\n29 | Refl -> applySing no _\r\n | ^\r\n}}}\r\n\r\nNote that this is distinct from #15142, as this is still reproducible on HEAD, even after commit 030211d21207dabb7a4bf21cc9af6fa5eb066db1.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1Matthías Páll GissurarsonMatthías Páll Gissurarsonhttps://gitlab.haskell.org/ghc/ghc/-/issues/23258-fdefer-typed-holes will raise "(deferred type error)" exception, and that na...2023-06-10T12:20:55Zjwaldmann-fdefer-typed-holes will raise "(deferred type error)" exception, and that name looks wrongwith ghc-9.6.1,
```
:set -fdefer-typed-holes
ghci> x = [True,_] -- gives warning, as expected
ghci> print x
[True,*** Exception: <interactive>:11:11: error: [GHC-88464]
...
(deferred type error)
```
that last line looks wrong to me, s...with ghc-9.6.1,
```
:set -fdefer-typed-holes
ghci> x = [True,_] -- gives warning, as expected
ghci> print x
[True,*** Exception: <interactive>:11:11: error: [GHC-88464]
...
(deferred type error)
```
that last line looks wrong to me, since there is no type error. Documentation says "a hole ... will behave like undefined", and for that I would get no type error.https://gitlab.haskell.org/ghc/ghc/-/issues/23004Typed holes should take record wildcards into account2023-02-21T15:33:32ZJaro ReindersTyped holes should take record wildcards into account## Summary
When using record wildcards together with typed holes, you don't get very useful information.
This is especially painful if you are using record wildcards as a workaround for #12376 (as suggested in comment https://gitlab.ha...## Summary
When using record wildcards together with typed holes, you don't get very useful information.
This is especially painful if you are using record wildcards as a workaround for #12376 (as suggested in comment https://gitlab.haskell.org/ghc/ghc/-/issues/12376#note_125684). And also if you are using typed holes in combination with tools like [wingman](https://haskellwingman.dev/) which gives typed holes superpowers.
## Steps to reproduce
```haskell
{-# LANGUAGE RecordWildCards #-}
data Foo = Foo {foo :: Int}
test :: Foo
test = Foo {..}
where
foo = _
```
Gives the suggestion:
```
T.hs:8:11: error:
• Found hole: _ :: p
Where: ‘p’ is a rigid type variable bound by
the inferred type of foo :: p
at T.hs:8:5-11
• In an equation for ‘foo’: foo = _
In an equation for ‘test’:
test
= Foo {..}
where
foo = _
• Relevant bindings include
foo :: p (bound at T.hs:8:5)
test :: Foo (bound at T.hs:6:1)
|
8 | foo = _
| ^
```
## Expected behavior
GHC should say that the type of the hole must be `Int` because that is the type of the `foo` field. The typed holes should be consistent with the type error you get when you use a wrong type, e.g.:
```haskell
{-# LANGUAGE RecordWildCards #-}
data Foo = Foo {foo :: Int}
test :: Foo
test = Foo {..}
where
foo = ()
```
Gives the error:
```
T.hs:6:13: error:
• Couldn't match expected type ‘Int’ with actual type ‘()’
• In the ‘foo’ field of a record
In the expression: Foo {..}
In an equation for ‘test’:
test
= Foo {..}
where
foo = ()
|
6 | test = Foo {..}
| ^^
```
So GHC does know that `foo :: Int` should hold.
## Environment
* GHC version used: 9.2.4https://gitlab.haskell.org/ghc/ghc/-/issues/20860Multiple occurrence of the same out-of-scope identifier should be commoned up2022-01-03T21:58:10ZRichard Eisenbergrae@richarde.devMultiple occurrence of the same out-of-scope identifier should be commoned upIf I say `x = _blah _blah`, I get two errors, one for each of the out-of-scope `_blah`s. What's strange is that the two have different types! Though the example here won't work for any (monomorphic) type, in more elaborate cases, users m...If I say `x = _blah _blah`, I get two errors, one for each of the out-of-scope `_blah`s. What's strange is that the two have different types! Though the example here won't work for any (monomorphic) type, in more elaborate cases, users might want to find some function or variable that fits in several different places in their code. GHC should do them the favor of giving each occurrence of the same out-of-scope identifier the same type. Note that `_` is not an identifier, so multiple uses of `_` would indeed be different.
Inspired by [this YouTube comment](https://www.youtube.com/watch?v=5OrSYF5ybhI&lc=UgzZpbkZhrGD4_3_QLR4AaABAg).
cc @Tritlohttps://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/18877Premature specialization of numeric literals with Typed Holes2020-11-08T16:38:30ZparsonsmattPremature specialization of numeric literals with Typed Holes## Summary
Numeric literals are specialized to `Integer` which trips up the hole fit algorithm.
## Steps to reproduce
Suppose I forgot about `Map.singleton`, and I wrote this code:
```haskell
import qualified Data.Map as Map
what ::...## Summary
Numeric literals are specialized to `Integer` which trips up the hole fit algorithm.
## Steps to reproduce
Suppose I forgot about `Map.singleton`, and I wrote this code:
```haskell
import qualified Data.Map as Map
what :: Map.Map String Int
what = _f "hello" 1
```
GHC 8.10.2 will suggest `mempty`. The reason is that `1` gets specialized to `Integer`, which means that `_f :: String -> Integer -> Map String Int`, and there are no valid fits for it. We can fix this by either changing `Int` to `Integer` or adding a type annotation to `1`.
If we generalize the `Map`, this still doesn't work:
```haskell
what :: forall a. Num a => Map.Map String a
what = _f "hello" 1
```
```
/home/matt/map.hs:6:8: error:
• Found hole: _f :: [Char] -> Integer -> Map.Map String a
Where: ‘a’ is a rigid type variable bound by
the type signature for:
what :: forall a. Num a => Map.Map String a
at /home/matt/map.hs:5:1-43
Or perhaps ‘_f’ is mis-spelled, or not in scope
• In the expression: _f
In the expression: _f "hello" 1
In an equation for ‘what’: what = _f "hello" 1
• Relevant bindings include
what :: Map.Map String a (bound at /home/matt/map.hs:6:1)
Constraints include Num a (from /home/matt/map.hs:5:1-43)
Valid hole fits include
mempty :: forall a. Monoid a => a
with mempty @([Char] -> Integer -> Map.Map String a)
(imported from ‘Prelude’ at /home/matt/map.hs:1:1
(and originally defined in ‘GHC.Base’))
|
6 | what = _f "hello" 1
| ^^
```
The only way to get the right suggestion is to force `1` to remain polymorphic with a type signature.
```haskell
{-# language ScopedTypeVariables #-}
import qualified Data.Map as Map
what :: forall a. Num a => Map.Map String a
what = _f "hello" (1 :: a)
```
```
/home/matt/map.hs:6:8: error:
• Found hole: _f :: [Char] -> a -> Map.Map String a
Where: ‘a’ is a rigid type variable bound by
the type signature for:
what :: forall a. Num a => Map.Map String a
at /home/matt/map.hs:5:1-43
Or perhaps ‘_f’ is mis-spelled, or not in scope
• In the expression: _f
In the expression: _f "hello" (1 :: a)
In an equation for ‘what’: what = _f "hello" (1 :: a)
• Relevant bindings include
what :: Map.Map String a (bound at /home/matt/map.hs:6:1)
Constraints include Num a (from /home/matt/map.hs:5:1-43)
Valid hole fits include
Map.singleton :: forall k a. k -> a -> Map.Map k a
with Map.singleton @String @a
(imported qualified from ‘Data.Map’ at /home/matt/map.hs:3:1-32
(and originally defined in ‘Data.Map.Internal’))
mempty :: forall a. Monoid a => a
with mempty @([Char] -> a -> Map.Map String a)
(imported from ‘Prelude’ at /home/matt/map.hs:1:1
(and originally defined in ‘GHC.Base’))
|
6 | what = _f "hello" (1 :: a)
| ^^
```
Curiously, this also fails to suggest `Map.singleton`:
```haskell
{-# language AllowAmbiguousTypes, ScopedTypeVariables #-}
import qualified Data.Map as Map
what :: forall a. Num a => Map.Map String Int
what = _f "hello" (1 :: a)
```
It can't unify `_f :: String -> a -> Map.Map String Int` with `Map.singleton :: String -> Int -> Map.Map String Int`.
I tried this with `mempty` instead of `1`, but that actually works:
```haskell
import qualified Data.Map as Map
import Data.Monoid (Sum)
what :: Map.Map String (Sum Int)
what = _f "hello" mempty
```
```
[1 of 1] Compiling Main ( /home/matt/map.hs, interpreted )
/home/matt/map.hs:5:8: error:
• Found hole: _f :: [Char] -> t0 -> Map.Map String (Sum Int)
Where: ‘t0’ is an ambiguous type variable
Or perhaps ‘_f’ is mis-spelled, or not in scope
• In the expression: _f
In the expression: _f "hello" mempty
In an equation for ‘what’: what = _f "hello" mempty
• Relevant bindings include
what :: Map.Map String (Sum Int) (bound at /home/matt/map.hs:5:1)
Valid hole fits include
Map.delete :: forall k a. Ord k => k -> Map.Map k a -> Map.Map k a
with Map.delete @String @(Sum Int)
(imported qualified from ‘Data.Map’ at /home/matt/map.hs:1:1-32
(and originally defined in ‘Data.Map.Internal’))
Map.singleton :: forall k a. k -> a -> Map.Map k a
with Map.singleton @String @(Sum Int)
(imported qualified from ‘Data.Map’ at /home/matt/map.hs:1:1-32
(and originally defined in ‘Data.Map.Internal’))
seq :: forall a b. a -> b -> b
with seq @[Char] @(Map.Map String (Sum Int))
(imported from ‘Prelude’ at /home/matt/map.hs:1:1
(and originally defined in ‘GHC.Prim’))
|
5 | what = _f "hello" mempty
| ^^
/home/matt/map.hs:5:19: error:
• Ambiguous type variable ‘t0’ arising from a use of ‘mempty’
prevents the constraint ‘(Monoid t0)’ from being solved.
Probable fix: use a type annotation to specify what ‘t0’ should be.
These potential instances exist:
instance Num a => Monoid (Sum a)
-- Defined in ‘base-4.14.1.0:Data.Semigroup.Internal’
instance Ord k => Monoid (Map.Map k v)
-- Defined in ‘Data.Map.Internal’
instance Monoid a => Monoid (IO a) -- Defined in ‘GHC.Base’
...plus 9 others
...plus 22 instances involving out-of-scope types
(use -fprint-potential-instances to see them all)
• In the second argument of ‘_f’, namely ‘mempty’
In the expression: _f "hello" mempty
In an equation for ‘what’: what = _f "hello" mempty
|
5 | what = _f "hello" mempty
| ^^^^^^
Failed, no modules loaded.
```
Surprisingly enough, it suggests `seq`, which relies on the `Monoid` instance for `Map`! But it doesn't suggest `mempty` which *should* fit with `mempty @(_ -> Map _ _)` (via `Monoid r => Monoid (x -> r)`).
## Expected behavior
Instead of specializing `1 :: Num a => a` to `Integer` and then searching for hole fits, search for hole fits with the general signature. eg `_f :: Num a => String -> a -> Map String Int`. `Map.singleton` (as a valid specialization of the typed hole) should fit.
## Environment
* GHC version used: 8.10.2
Optional:
* Operating System:
* System Architecture:https://gitlab.haskell.org/ghc/ghc/-/issues/16312Optimization + adding an INLINE pragma triggers Core Lint error (Type of case...2020-04-23T14:29:22ZRyan ScottOptimization + adding an INLINE pragma triggers Core Lint error (Type of case alternatives not the same as the annotation on case)Here's a seemingly innocuous program, minimized from the `kan-extensions` library:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
module Bug where
newtype Curried g h a =
Curried { runCurried :: forall r. g (a -> r) -> h r ...Here's a seemingly innocuous program, minimized from the `kan-extensions` library:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
module Bug where
newtype Curried g h a =
Curried { runCurried :: forall r. g (a -> r) -> h r }
instance Functor g => Functor (Curried g h) where
fmap f (Curried g) = Curried (g . fmap (.f))
instance (Functor g, g ~ h) => Applicative (Curried g h) where
pure a = Curried (fmap ($a))
Curried mf <*> Curried ma = Curried (ma . mf . fmap (.))
{-# INLINE (<*>) #-}
-- The Core Lint error goes away if you remove this INLINE pragma
```
However, it triggers a Core Lint error on GHC 8.2.2 through HEAD if you compile it with `-O` and `-dcore-lint`:
```
$ /opt/ghc/8.6.3/bin/ghc -fforce-recomp -dcore-lint Bug.hs -O
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Simplifier ***
<no location info>: warning:
In the expression: (case heq_sel
@ (* -> *)
@ (* -> *)
@ h_a1eC
@ h_a1eC
($d~_a1eE
`cast` (((~) <* -> *>_N co_a1hx <h_a1eC>_N)_R ; N:~[0]
<*
-> *>_N <h_a1eC>_N <h_a1eC>_N
:: (g_a1eB ~ h_a1eC) ~R# (h_a1eC ~~ h_a1eC)))
of co_X1ij
{ __DEFAULT ->
(\ (@ a_a1fg)
(@ b_a1fh)
(ds_d1yw :: Curried h_a1eC h_a1eC (a_a1fg -> b_a1fh))
(ds_d1yx :: Curried h_a1eC h_a1eC a_a1fg)
(@ r_a1fn) ->
let {
g_X1zi
:: h_a1eC (b_a1fh -> r_a1fn)
-> h_a1eC ((a_a1fg -> b_a1fh) -> a_a1fg -> r_a1fn)
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=False, Value=False, ConLike=False,
WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 30 0}]
g_X1zi
= fmap
@ h_a1eC
($dFunctor_a1eD
`cast` ((Functor co_a1hx)_R
:: Functor g_a1eB ~R# Functor h_a1eC))
@ (b_a1fh -> r_a1fn)
@ ((a_a1fg -> b_a1fh) -> a_a1fg -> r_a1fn)
(. @ b_a1fh @ r_a1fn @ a_a1fg) } in
\ (x_X1zn :: h_a1eC (b_a1fh -> r_a1fn)) ->
(ds_d1yx
`cast` (N:Curried[0] <h_a1eC>_R <h_a1eC>_R <a_a1fg>_N
:: Curried h_a1eC h_a1eC a_a1fg
~R# (forall r. h_a1eC (a_a1fg -> r) -> h_a1eC r)))
@ r_a1fn
((ds_d1yw
`cast` (N:Curried[0] <h_a1eC>_R <h_a1eC>_R <a_a1fg -> b_a1fh>_N
:: Curried h_a1eC h_a1eC (a_a1fg -> b_a1fh)
~R# (forall r.
h_a1eC ((a_a1fg -> b_a1fh) -> r) -> h_a1eC r)))
@ (a_a1fg -> r_a1fn) (g_X1zi x_X1zn)))
`cast` (forall (a :: <*>_N) (b :: <*>_N).
<Curried h_a1eC h_a1eC (a -> b)>_R
->_R <Curried h_a1eC h_a1eC a>_R
->_R Sym (N:Curried[0] <h_a1eC>_R <h_a1eC>_R <b>_N)
:: (forall a b.
Curried h_a1eC h_a1eC (a -> b)
-> Curried h_a1eC h_a1eC a
-> forall r. h_a1eC (b -> r) -> h_a1eC r)
~R# (forall a b.
Curried h_a1eC h_a1eC (a -> b)
-> Curried h_a1eC h_a1eC a -> Curried h_a1eC h_a1eC b))
})
@ b_a1gi
@ b_a1gi
((<$
@ (Curried g_a1eB h_a1eC)
($dFunctor_s1zH
`cast` ((Functor (Curried (Sym co_a1hx) <h_a1eC>_N)_N)_R
:: Functor (Curried h_a1eC h_a1eC)
~R# Functor (Curried g_a1eB h_a1eC)))
@ (b_a1gi -> b_a1gi)
@ a_a1gh
(breakpoint @ b_a1gi)
a1_a1z1)
`cast` (Sym (Curried
(Sub (Sym co_a1hx)) <h_a1eC>_R <b_a1gi -> b_a1gi>_N)_R
:: Curried g_a1eB h_a1eC (b_a1gi -> b_a1gi)
~R# Curried h_a1eC h_a1eC (b_a1gi -> b_a1gi)))
(a2_a1z2
`cast` (Sym (Curried (Sub (Sym co_a1hx)) <h_a1eC>_R <b_a1gi>_N)_R
:: Curried g_a1eB h_a1eC b_a1gi ~R# Curried h_a1eC h_a1eC b_a1gi))
Type of case alternatives not the same as the annotation on case:
Actual type: forall a b.
Curried h_a1eC h_a1eC (a -> b)
-> Curried h_a1eC h_a1eC a -> Curried h_a1eC h_a1eC b
Annotation on case: forall a b.
Curried g_a1eB h_a1eC (a -> b)
-> Curried g_a1eB h_a1eC a -> Curried g_a1eB h_a1eC b
```
The size of the `-dcore-lint` output is enormous, so I'll post it separately as an attachment.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Optimization + adding an INLINE pragma triggers Core Lint error (Type of case alternatives not the same as the annotation on case)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Here's a seemingly innocuous program, minimized from the `kan-extensions` library:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE RankNTypes #-}\r\nmodule Bug where\r\n\r\nnewtype Curried g h a =\r\n Curried { runCurried :: forall r. g (a -> r) -> h r }\r\n\r\ninstance Functor g => Functor (Curried g h) where\r\n fmap f (Curried g) = Curried (g . fmap (.f))\r\n\r\ninstance (Functor g, g ~ h) => Applicative (Curried g h) where\r\n pure a = Curried (fmap ($a))\r\n Curried mf <*> Curried ma = Curried (ma . mf . fmap (.))\r\n {-# INLINE (<*>) #-}\r\n -- The Core Lint error goes away if you remove this INLINE pragma\r\n}}}\r\n\r\nHowever, it triggers a Core Lint error on GHC 8.2.2 through HEAD if you compile it with `-O` and `-dcore-lint`:\r\n\r\n{{{\r\n$ /opt/ghc/8.6.3/bin/ghc -fforce-recomp -dcore-lint Bug.hs -O\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n*** Core Lint errors : in result of Simplifier ***\r\n<no location info>: warning:\r\n In the expression: (case heq_sel\r\n @ (* -> *)\r\n @ (* -> *)\r\n @ h_a1eC\r\n @ h_a1eC\r\n ($d~_a1eE\r\n `cast` (((~) <* -> *>_N co_a1hx <h_a1eC>_N)_R ; N:~[0]\r\n <*\r\n -> *>_N <h_a1eC>_N <h_a1eC>_N\r\n :: (g_a1eB ~ h_a1eC) ~R# (h_a1eC ~~ h_a1eC)))\r\n of co_X1ij\r\n { __DEFAULT ->\r\n (\\ (@ a_a1fg)\r\n (@ b_a1fh)\r\n (ds_d1yw :: Curried h_a1eC h_a1eC (a_a1fg -> b_a1fh))\r\n (ds_d1yx :: Curried h_a1eC h_a1eC a_a1fg)\r\n (@ r_a1fn) ->\r\n let {\r\n g_X1zi\r\n :: h_a1eC (b_a1fh -> r_a1fn)\r\n -> h_a1eC ((a_a1fg -> b_a1fh) -> a_a1fg -> r_a1fn)\r\n [LclId,\r\n Unf=Unf{Src=<vanilla>, TopLvl=False, Value=False, ConLike=False,\r\n WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 30 0}]\r\n g_X1zi\r\n = fmap\r\n @ h_a1eC\r\n ($dFunctor_a1eD\r\n `cast` ((Functor co_a1hx)_R\r\n :: Functor g_a1eB ~R# Functor h_a1eC))\r\n @ (b_a1fh -> r_a1fn)\r\n @ ((a_a1fg -> b_a1fh) -> a_a1fg -> r_a1fn)\r\n (. @ b_a1fh @ r_a1fn @ a_a1fg) } in\r\n \\ (x_X1zn :: h_a1eC (b_a1fh -> r_a1fn)) ->\r\n (ds_d1yx\r\n `cast` (N:Curried[0] <h_a1eC>_R <h_a1eC>_R <a_a1fg>_N\r\n :: Curried h_a1eC h_a1eC a_a1fg\r\n ~R# (forall r. h_a1eC (a_a1fg -> r) -> h_a1eC r)))\r\n @ r_a1fn\r\n ((ds_d1yw\r\n `cast` (N:Curried[0] <h_a1eC>_R <h_a1eC>_R <a_a1fg -> b_a1fh>_N\r\n :: Curried h_a1eC h_a1eC (a_a1fg -> b_a1fh)\r\n ~R# (forall r.\r\n h_a1eC ((a_a1fg -> b_a1fh) -> r) -> h_a1eC r)))\r\n @ (a_a1fg -> r_a1fn) (g_X1zi x_X1zn)))\r\n `cast` (forall (a :: <*>_N) (b :: <*>_N).\r\n <Curried h_a1eC h_a1eC (a -> b)>_R\r\n ->_R <Curried h_a1eC h_a1eC a>_R\r\n ->_R Sym (N:Curried[0] <h_a1eC>_R <h_a1eC>_R <b>_N)\r\n :: (forall a b.\r\n Curried h_a1eC h_a1eC (a -> b)\r\n -> Curried h_a1eC h_a1eC a\r\n -> forall r. h_a1eC (b -> r) -> h_a1eC r)\r\n ~R# (forall a b.\r\n Curried h_a1eC h_a1eC (a -> b)\r\n -> Curried h_a1eC h_a1eC a -> Curried h_a1eC h_a1eC b))\r\n })\r\n @ b_a1gi\r\n @ b_a1gi\r\n ((<$\r\n @ (Curried g_a1eB h_a1eC)\r\n ($dFunctor_s1zH\r\n `cast` ((Functor (Curried (Sym co_a1hx) <h_a1eC>_N)_N)_R\r\n :: Functor (Curried h_a1eC h_a1eC)\r\n ~R# Functor (Curried g_a1eB h_a1eC)))\r\n @ (b_a1gi -> b_a1gi)\r\n @ a_a1gh\r\n (breakpoint @ b_a1gi)\r\n a1_a1z1)\r\n `cast` (Sym (Curried\r\n (Sub (Sym co_a1hx)) <h_a1eC>_R <b_a1gi -> b_a1gi>_N)_R\r\n :: Curried g_a1eB h_a1eC (b_a1gi -> b_a1gi)\r\n ~R# Curried h_a1eC h_a1eC (b_a1gi -> b_a1gi)))\r\n (a2_a1z2\r\n `cast` (Sym (Curried (Sub (Sym co_a1hx)) <h_a1eC>_R <b_a1gi>_N)_R\r\n :: Curried g_a1eB h_a1eC b_a1gi ~R# Curried h_a1eC h_a1eC b_a1gi))\r\n Type of case alternatives not the same as the annotation on case:\r\n Actual type: forall a b.\r\n Curried h_a1eC h_a1eC (a -> b)\r\n -> Curried h_a1eC h_a1eC a -> Curried h_a1eC h_a1eC b\r\n Annotation on case: forall a b.\r\n Curried g_a1eB h_a1eC (a -> b)\r\n -> Curried g_a1eB h_a1eC a -> Curried g_a1eB h_a1eC b\r\n}}}\r\n\r\nThe size of the `-dcore-lint` output is enormous, so I'll post it separately as an attachment.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/15697Typed holes inferring a more polymorphic type2019-07-08T11:15:20ZsreenidhiTyped holes inferring a more polymorphic typeConsider these two snippets.
```hs
testFailure :: Char
testFailure =
let x = id _
in x
```
Suggestions provided were
```
/home/sreenidhi/Experiments/TypedHole.hs:3:14: error:
• Found hole: _ :: a
Where: ‘a’ is a rigid t...Consider these two snippets.
```hs
testFailure :: Char
testFailure =
let x = id _
in x
```
Suggestions provided were
```
/home/sreenidhi/Experiments/TypedHole.hs:3:14: error:
• Found hole: _ :: a
Where: ‘a’ is a rigid type variable bound by
the inferred type of x :: a
at /home/sreenidhi/Experiments/TypedHole.hs:3:7-14
• In the first argument of ‘id’, namely ‘_’
In the expression: id _
In an equation for ‘x’: x = id _
• Relevant bindings include
x :: a (bound at /home/sreenidhi/Experiments/TypedHole.hs:3:7)
testFailure :: Char
(bound at /home/sreenidhi/Experiments/TypedHole.hs:2:1)
```
whereas for this one
```hs
testSuccess :: Char
testSuccess = _
```
It correctly suggests
```
/home/sreenidhi/Experiments/TypedHole.hs:7:15: error:
• Found hole: _ :: Char
• In the expression: _
In an equation for ‘testSuccess’: testSuccess = _
• Relevant bindings include
testSuccess :: Char
(bound at /home/sreenidhi/Experiments/TypedHole.hs:7:1)
Valid hole fits include
testSuccess :: Char
(bound at /home/sreenidhi/Experiments/TypedHole.hs:7:1)
testFailure :: Char
(defined at /home/sreenidhi/Experiments/TypedHole.hs:2:1)
maxBound :: forall a. Bounded a => a
with maxBound @Char
(imported from ‘Prelude’ at /home/sreenidhi/Experiments/TypedHole.hs:1:1
(and originally defined in ‘GHC.Enum’))
minBound :: forall a. Bounded a => a
with minBound @Char
(imported from ‘Prelude’ at /home/sreenidhi/Experiments/TypedHole.hs:1:1
(and originally defined in ‘GHC.Enum’))
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Typed holes inferring a more polymorphic type","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider these two snippets.\r\n\r\n{{{#!hs\r\ntestFailure :: Char\r\ntestFailure =\r\n let x = id _\r\n in x\r\n}}}\r\n\r\n\r\nSuggestions provided were\r\n{{{\r\n/home/sreenidhi/Experiments/TypedHole.hs:3:14: error:\r\n • Found hole: _ :: a\r\n Where: ‘a’ is a rigid type variable bound by\r\n the inferred type of x :: a\r\n at /home/sreenidhi/Experiments/TypedHole.hs:3:7-14\r\n • In the first argument of ‘id’, namely ‘_’\r\n In the expression: id _\r\n In an equation for ‘x’: x = id _\r\n • Relevant bindings include\r\n x :: a (bound at /home/sreenidhi/Experiments/TypedHole.hs:3:7)\r\n testFailure :: Char\r\n (bound at /home/sreenidhi/Experiments/TypedHole.hs:2:1)\r\n\r\n}}}\r\n\r\nwhereas for this one\r\n\r\n{{{#!hs\r\ntestSuccess :: Char\r\ntestSuccess = _\r\n}}}\r\n\r\nIt correctly suggests\r\n\r\n{{{\r\n/home/sreenidhi/Experiments/TypedHole.hs:7:15: error:\r\n • Found hole: _ :: Char\r\n • In the expression: _\r\n In an equation for ‘testSuccess’: testSuccess = _\r\n • Relevant bindings include\r\n testSuccess :: Char\r\n (bound at /home/sreenidhi/Experiments/TypedHole.hs:7:1)\r\n Valid hole fits include\r\n testSuccess :: Char\r\n (bound at /home/sreenidhi/Experiments/TypedHole.hs:7:1)\r\n testFailure :: Char\r\n (defined at /home/sreenidhi/Experiments/TypedHole.hs:2:1)\r\n maxBound :: forall a. Bounded a => a\r\n with maxBound @Char\r\n (imported from ‘Prelude’ at /home/sreenidhi/Experiments/TypedHole.hs:1:1\r\n (and originally defined in ‘GHC.Enum’))\r\n minBound :: forall a. Bounded a => a\r\n with minBound @Char\r\n (imported from ‘Prelude’ at /home/sreenidhi/Experiments/TypedHole.hs:1:1\r\n (and originally defined in ‘GHC.Enum’))\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15677Valid hole fits and GADT type variable names2021-09-07T15:56:45ZRyan ScottValid hole fits and GADT type variable namesConsider the following code:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
module Foo where
import Data.Kind
data HList :: [...Consider the following code:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
module Foo where
import Data.Kind
data HList :: [Type] -> Type where
HNil :: HList '[]
HCons :: x -> HList xs -> HList (x:xs)
foo :: HList a -> HList a
foo HNil = HNil
foo (HCons (b :: bType) bs) = HCons _ bs
```
Here is the suggestion that the typed hole in `foo` provides:
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Foo ( Bug.hs, Bug.o )
Bug.hs:16:37: error:
• Found hole: _ :: x
Where: ‘x’ is a rigid type variable bound by
a pattern with constructor:
HCons :: forall x (xs :: [*]). x -> HList xs -> HList (x : xs),
in an equation for ‘foo’
at Bug.hs:16:6-26
• In the first argument of ‘HCons’, namely ‘_’
In the expression: HCons _ bs
In an equation for ‘foo’: foo (HCons (b :: bType) bs) = HCons _ bs
• Relevant bindings include
bs :: HList xs (bound at Bug.hs:16:25)
b :: x (bound at Bug.hs:16:13)
foo :: HList a -> HList a (bound at Bug.hs:15:1)
Constraints include a ~ (x : xs) (from Bug.hs:16:6-26)
Valid hole fits include b :: x (bound at Bug.hs:16:13)
|
16 | foo (HCons (b :: bType) bs) = HCons _ bs
| ^
```
One thing immediately stands out here: the hole has type `x`, but `x` appears no where in the definition of `foo`! I had expected this suggestion to mention `bType`, since I went through the effort of declaring `b` to have that type through a pattern signature, but GHC instead uses types from the definition of the `HCons` constructor itself. This seems less than ideal, since one would expect GHC to only ever mention types that are lexically in scope at a particular definition site.
One thing which complicates this idea is that there can be multiple in-scope type variables that all refer to the same type. For instance, if I define this function:
```hs
bar :: HList a -> HList a -> HList a
bar HNil HNil = HNil
bar (HCons (b :: bType) bs) (HCons (c :: cType) cs) = HCons _ bs
```
What should the suggested type of the hole be: `bType`, or `cType`? Either choice is equally valid. After talking with Tritlo and simonpj about this, we came to the consensus that we should just pick one of the type variables to report at the top of the error message:
```
• Found hole: _ :: bType
```
And then later in the message, include any type variable synonyms that have been brought into scope (via pattern signatures or otherwise). I imagine this might look something like:
```
• Type variable synonyms include
`cType` equals `bType`
```
This is quite similar to an existing feature of valid hole fits where we report `Constraints include`. (Indeed, we briefly considered just reporting these type variable synonyms as explicit equality constraints, but doing so would be somewhat misleading, since that's not how pattern signatures actually work in practice.)
One implementation challenge is to figure out how to construct a mapping from `x` to `bType`. One place where inspiration can be drawn from is the `ATyVar` constructor of `TcTyThing`:
```hs
data TcTyThing
= ...
| ATyVar Name TcTyVar -- The type variable to which the lexically scoped type
-- variable is bound. We only need the Name
-- for error-message purposes; it is the corresponding
-- Name in the domain of the envt
```
`ATyVar` already stores a "reverse mapping" of sorts to give better a more accurate `Name` in the event that it is pretty-printed, which is quite similar to what we need to do with `x` and `bType`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | Tritlo |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Valid hole fits and GADT type variable names","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["GADTs","TypedHoles,"],"differentials":[],"test_case":"","architecture":"","cc":["Tritlo"],"type":"Bug","description":"Consider the following code:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Foo where\r\n\r\nimport Data.Kind\r\n\r\ndata HList :: [Type] -> Type where\r\n HNil :: HList '[]\r\n HCons :: x -> HList xs -> HList (x:xs)\r\n\r\nfoo :: HList a -> HList a\r\nfoo HNil = HNil\r\nfoo (HCons (b :: bType) bs) = HCons _ bs\r\n}}}\r\n\r\nHere is the suggestion that the typed hole in `foo` provides:\r\n\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Foo ( Bug.hs, Bug.o )\r\n\r\nBug.hs:16:37: error:\r\n • Found hole: _ :: x\r\n Where: ‘x’ is a rigid type variable bound by\r\n a pattern with constructor:\r\n HCons :: forall x (xs :: [*]). x -> HList xs -> HList (x : xs),\r\n in an equation for ‘foo’\r\n at Bug.hs:16:6-26\r\n • In the first argument of ‘HCons’, namely ‘_’\r\n In the expression: HCons _ bs\r\n In an equation for ‘foo’: foo (HCons (b :: bType) bs) = HCons _ bs\r\n • Relevant bindings include\r\n bs :: HList xs (bound at Bug.hs:16:25)\r\n b :: x (bound at Bug.hs:16:13)\r\n foo :: HList a -> HList a (bound at Bug.hs:15:1)\r\n Constraints include a ~ (x : xs) (from Bug.hs:16:6-26)\r\n Valid hole fits include b :: x (bound at Bug.hs:16:13)\r\n |\r\n16 | foo (HCons (b :: bType) bs) = HCons _ bs\r\n | ^\r\n}}}\r\n\r\nOne thing immediately stands out here: the hole has type `x`, but `x` appears no where in the definition of `foo`! I had expected this suggestion to mention `bType`, since I went through the effort of declaring `b` to have that type through a pattern signature, but GHC instead uses types from the definition of the `HCons` constructor itself. This seems less than ideal, since one would expect GHC to only ever mention types that are lexically in scope at a particular definition site.\r\n\r\nOne thing which complicates this idea is that there can be multiple in-scope type variables that all refer to the same type. For instance, if I define this function:\r\n\r\n{{{#!hs\r\nbar :: HList a -> HList a -> HList a\r\nbar HNil HNil = HNil\r\nbar (HCons (b :: bType) bs) (HCons (c :: cType) cs) = HCons _ bs\r\n}}}\r\n\r\nWhat should the suggested type of the hole be: `bType`, or `cType`? Either choice is equally valid. After talking with Tritlo and simonpj about this, we came to the consensus that we should just pick one of the type variables to report at the top of the error message:\r\n\r\n{{{\r\n • Found hole: _ :: bType\r\n}}}\r\n\r\nAnd then later in the message, include any type variable synonyms that have been brought into scope (via pattern signatures or otherwise). I imagine this might look something like:\r\n\r\n{{{\r\n • Type variable synonyms include\r\n `cType` equals `bType`\r\n}}}\r\n\r\nThis is quite similar to an existing feature of valid hole fits where we report `Constraints include`. (Indeed, we briefly considered just reporting these type variable synonyms as explicit equality constraints, but doing so would be somewhat misleading, since that's not how pattern signatures actually work in practice.)\r\n\r\nOne implementation challenge is to figure out how to construct a mapping from `x` to `bType`. One place where inspiration can be drawn from is the `ATyVar` constructor of `TcTyThing`:\r\n\r\n{{{#!hs\r\ndata TcTyThing\r\n = ...\r\n | ATyVar Name TcTyVar -- The type variable to which the lexically scoped type\r\n -- variable is bound. We only need the Name\r\n -- for error-message purposes; it is the corresponding\r\n -- Name in the domain of the envt\r\n}}}\r\n\r\n`ATyVar` already stores a \"reverse mapping\" of sorts to give better a more accurate `Name` in the event that it is pretty-printed, which is quite similar to what we need to do with `x` and `bType`.","type_of_failure":"OtherFailure","blocking":[]} -->⊥https://gitlab.haskell.org/ghc/ghc/-/issues/15401Weird GHCi bug2019-07-07T18:05:05ZAlexey VagarenkoWeird GHCi bugTake a look at this GHCi session:
```hs
$ ghci
GHCi, version 8.4.3: http://www.haskell.org/ghc/ :? for help
```
type `do {_}`
```hs
Prelude> do {_} ...Take a look at this GHCi session:
```hs
$ ghci
GHCi, version 8.4.3: http://www.haskell.org/ghc/ :? for help
```
type `do {_}`
```hs
Prelude> do {_}
<interactive>:1:5: error:
* Found hole: _ :: t
Where: `t' is a rigid type variable bound by
the inferred type of it :: t
at <interactive>:1:1-6
* In a stmt of a 'do' block: _
In the expression: do _
In an equation for `it': it = do _
* Relevant bindings include it :: t (bound at <interactive>:1:1)
Valid substitutions include
undefined :: forall (a :: TYPE r).
GHC.Stack.Types.HasCallStack =>
a
(imported from `Prelude' (and originally defined in `GHC.Err'))
```
looks ok
type `()`
```hs
Prelude> ()
()
```
ok
type `do {_}` again
```hs
Prelude> do {_}
<interactive>:3:5: error:
* Found hole: _ :: t
Where: `t' is a rigid type variable bound by
the inferred type of it :: t
at <interactive>:3:1-6
* In a stmt of a 'do' block: _
In the expression: do _
In an equation for `it': it = do _
* Relevant bindings include it :: t (bound at <interactive>:3:1)
Valid substitutions include
undefined :: forall (a :: TYPE r).
GHC.Stack.Types.HasCallStack =>
a
(imported from `Prelude' (and originally defined in `GHC.Err'))
```
ok, same message
type `()` second type
```hs
Prelude> ()
()
```
ok,
type `do {_}` third time:
```hs
Prelude> do {_}
<interactive>:1:1: error:
GHC internal error: `Ghci1.it' is not in scope during type checking,
but it passed the renamer
tcl_env of environment: []
Prelude>
```
what's happening?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.4.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | GHCi |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Weird GHCi bug","status":"New","operating_system":"","component":"GHCi","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Take a look at this GHCi session:\r\n{{{#!hs\r\n$ ghci \r\nGHCi, version 8.4.3: http://www.haskell.org/ghc/ :? for help\r\n}}}\r\ntype `do {_}`\r\n{{{#!hs \r\nPrelude> do {_} \r\n \r\n<interactive>:1:5: error: \r\n * Found hole: _ :: t \r\n Where: `t' is a rigid type variable bound by \r\n the inferred type of it :: t \r\n at <interactive>:1:1-6 \r\n * In a stmt of a 'do' block: _ \r\n In the expression: do _ \r\n In an equation for `it': it = do _ \r\n * Relevant bindings include it :: t (bound at <interactive>:1:1) \r\n Valid substitutions include \r\n undefined :: forall (a :: TYPE r). \r\n GHC.Stack.Types.HasCallStack => \r\n a \r\n (imported from `Prelude' (and originally defined in `GHC.Err'))\r\n}}}\r\nlooks ok\r\n\r\ntype `()`\r\n{{{#!hs\r\nPrelude> () \r\n() \r\n}}}\r\nok\r\n\r\ntype `do {_}` again\r\n{{{#!hs\r\nPrelude> do {_} \r\n \r\n<interactive>:3:5: error: \r\n * Found hole: _ :: t \r\n Where: `t' is a rigid type variable bound by \r\n the inferred type of it :: t \r\n at <interactive>:3:1-6 \r\n * In a stmt of a 'do' block: _ \r\n In the expression: do _ \r\n In an equation for `it': it = do _ \r\n * Relevant bindings include it :: t (bound at <interactive>:3:1) \r\n Valid substitutions include \r\n undefined :: forall (a :: TYPE r). \r\n GHC.Stack.Types.HasCallStack => \r\n a \r\n (imported from `Prelude' (and originally defined in `GHC.Err'))\r\n}}}\r\nok, same message\r\n\r\ntype `()` second type\r\n{{{#!hs\r\nPrelude> () \r\n() \r\n}}}\r\nok,\r\n\r\ntype `do {_}` third time:\r\n{{{#!hs\r\nPrelude> do {_} \r\n \r\n<interactive>:1:1: error: \r\n GHC internal error: `Ghci1.it' is not in scope during type checking, \r\nbut it passed the renamer \r\n tcl_env of environment: [] \r\nPrelude> \r\n}}}\r\nwhat's happening?","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15321Typed holes in Template Haskell splices produce bewildering error messages2019-07-07T18:13:14ZRyan ScottTyped holes in Template Haskell splices produce bewildering error messagesIf you compile this program with GHC 8.4 or later:
```hs
{-# LANGUAGE TemplateHaskell #-}
module Bug where
foo :: String
foo = test
bar :: String
bar = $(_ "baz")
```
You'll be greeted with a rather strange error message:
```
$ /opt...If you compile this program with GHC 8.4 or later:
```hs
{-# LANGUAGE TemplateHaskell #-}
module Bug where
foo :: String
foo = test
bar :: String
bar = $(_ "baz")
```
You'll be greeted with a rather strange error message:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:8:7: error:
• GHC stage restriction:
‘foo’ is used in a top-level splice, quasi-quote, or annotation,
and must be imported, not defined locally
• In the untyped splice: $(_ "baz")
|
8 | bar = $(_ "baz")
| ^^^^^^^^^^
```
`foo` has nothing do with how `bar`'s RHS should be typechecked, so why is it being mentioned in the error message?
In contrast, GHC 8.2 and earlier gives you quite a nice error message:
```
$ /opt/ghc/8.2.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:8:9: error:
• Found hole: _ :: [Char] -> Language.Haskell.TH.Lib.ExpQ
• In the expression: _
In the expression: _ "baz"
In the untyped splice: $(_ "baz")
|
8 | bar = $(_ "baz")
| ^
```
Tritlo, my hunch is that the valid hole fits stuff is the culprit here. Do you think that perhaps when building the subsumption graph, we are trying to check the hole's type against that of `foo`, which causes the stage restriction error? If so, do you think it is possible to work around this?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ---------------- |
| Version | 8.4.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Template Haskell |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | Tritlo |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Typed holes in Template Haskell splices produce bewildering error messages","status":"New","operating_system":"","component":"Template Haskell","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypedHoles"],"differentials":[],"test_case":"","architecture":"","cc":["Tritlo"],"type":"Bug","description":"If you compile this program with GHC 8.4 or later:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TemplateHaskell #-}\r\nmodule Bug where\r\n\r\nfoo :: String\r\nfoo = test\r\n\r\nbar :: String\r\nbar = $(_ \"baz\")\r\n}}}\r\n\r\nYou'll be greeted with a rather strange error message:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:8:7: error:\r\n • GHC stage restriction:\r\n ‘foo’ is used in a top-level splice, quasi-quote, or annotation,\r\n and must be imported, not defined locally\r\n • In the untyped splice: $(_ \"baz\")\r\n |\r\n8 | bar = $(_ \"baz\")\r\n | ^^^^^^^^^^\r\n}}}\r\n\r\n`foo` has nothing do with how `bar`'s RHS should be typechecked, so why is it being mentioned in the error message?\r\n\r\nIn contrast, GHC 8.2 and earlier gives you quite a nice error message:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.2/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:8:9: error:\r\n • Found hole: _ :: [Char] -> Language.Haskell.TH.Lib.ExpQ\r\n • In the expression: _\r\n In the expression: _ \"baz\"\r\n In the untyped splice: $(_ \"baz\")\r\n |\r\n8 | bar = $(_ \"baz\")\r\n | ^\r\n}}}\r\n\r\nTritlo, my hunch is that the valid hole fits stuff is the culprit here. Do you think that perhaps when building the subsumption graph, we are trying to check the hole's type against that of `foo`, which causes the stage restriction error? If so, do you think it is possible to work around this?","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15202Internal error showing typed hole in GHCi2019-07-07T18:13:49ZDavid FeuerInternal error showing typed hole in GHCiRun `ghc --interactive`, and at the prompt type
```hs
default ()
fish :: Eq a => a; fish = undefined
foo :: String; foo = show _
```
The following error appears:
```
<interactive>:1:1: error:
GHC internal error: ‘Ghci1.$trModule’ ...Run `ghc --interactive`, and at the prompt type
```hs
default ()
fish :: Eq a => a; fish = undefined
foo :: String; foo = show _
```
The following error appears:
```
<interactive>:1:1: error:
GHC internal error: ‘Ghci1.$trModule’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: [r2CZ :-> Identifier[foo::String, TopLevelLet]]
```
I have not yet been able to reproduce this loading a module; it seems to need to be on the command line.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.5 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Internal error showing typed hole in GHCi","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypedHoles"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Run `ghc --interactive`, and at the prompt type\r\n\r\n{{{#!hs\r\ndefault ()\r\nfish :: Eq a => a; fish = undefined\r\nfoo :: String; foo = show _\r\n}}}\r\n\r\nThe following error appears:\r\n\r\n{{{\r\n<interactive>:1:1: error:\r\n GHC internal error: ‘Ghci1.$trModule’ is not in scope during type checking, but it passed the renamer\r\n tcl_env of environment: [r2CZ :-> Identifier[foo::String, TopLevelLet]]\r\n}}}\r\n\r\nI have not yet been able to reproduce this loading a module; it seems to need to be on the command line.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15076Typed hole with higher-rank kind causes GHC to panic (No skolem info)2019-07-07T18:14:23ZRyan ScottTyped hole with higher-rank kind causes GHC to panic (No skolem info)Spun out from #14040\#[ticket:15076\#comment:152359](https://gitlab.haskell.org//ghc/ghc/issues/15076#note_152359), which was different enough from the original program in #14040 to warrant its own ticket. The following program panics on...Spun out from #14040\#[ticket:15076\#comment:152359](https://gitlab.haskell.org//ghc/ghc/issues/15076#note_152359), which was different enough from the original program in #14040 to warrant its own ticket. The following program panics on every version of GHC from 8.0.2 onward:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
import Data.Proxy
foo :: forall (a :: Type)
(f :: forall (x :: a). Proxy x -> Type).
Proxy f -> ()
foo (_ :: _) = ()
```
```
$ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:12:11: error:ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.5.20180420 for x86_64-unknown-linux):
No skolem info:
[a_aZo[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:3224:5 in ghc:TcErrors
```8.8.1https://gitlab.haskell.org/ghc/ghc/-/issues/15037Running 1 twice, followed by a typed hole, in GHCi causes internal error2019-07-07T18:14:36ZRyan ScottRunning 1 twice, followed by a typed hole, in GHCi causes internal errorOriginally reported in #14996\##15037. You need GHC HEAD (i.e., more recent than GHC 8.4.1) to trigger this:
```
$ inplace/bin/ghc-stage2 --interactive
GHCi, version 8.5.20180413: http://www.haskell.org/ghc/ :? for help
Loaded GHCi con...Originally reported in #14996\##15037. You need GHC HEAD (i.e., more recent than GHC 8.4.1) to trigger this:
```
$ inplace/bin/ghc-stage2 --interactive
GHCi, version 8.5.20180413: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
λ> 1
1
λ> 1
1
λ> _
<interactive>:1:1: error:
GHC internal error: ‘Ghci1.it’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: []
```
And yes, running `1` //twice// seems to be critical to triggering this bug, for some reason.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.5 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | GHCi |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Running 1 twice, followed by a typed hole, in GHCi causes internal error","status":"New","operating_system":"","component":"GHCi","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypedHoles"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Originally reported in https://ghc.haskell.org/trac/ghc/ticket/14996#comment:2. You need GHC HEAD (i.e., more recent than GHC 8.4.1) to trigger this:\r\n\r\n{{{\r\n$ inplace/bin/ghc-stage2 --interactive\r\nGHCi, version 8.5.20180413: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\nλ> 1\r\n1\r\nλ> 1\r\n1\r\nλ> _\r\n\r\n<interactive>:1:1: error:\r\n GHC internal error: ‘Ghci1.it’ is not in scope during type checking, but it passed the renamer\r\n tcl_env of environment: []\r\n}}}\r\n\r\nAnd yes, running `1` //twice// seems to be critical to triggering this bug, for some reason.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15035Panic when using StaticPointers with typed holes2019-07-07T18:14:36ZutdemirPanic when using StaticPointers with typed holesAdding a type hole when there is a type variable in `StaticPtr` throws a GHC panic:
```hs
{-# LANGUAGE StaticPointers #-}
module Foo where
import Data.Typeable
import GHC.StaticPtr
foo :: Typeable a => StaticPtr a
foo = static _
```...Adding a type hole when there is a type variable in `StaticPtr` throws a GHC panic:
```hs
{-# LANGUAGE StaticPointers #-}
module Foo where
import Data.Typeable
import GHC.StaticPtr
foo :: Typeable a => StaticPtr a
foo = static _
```
```
[1 of 1] Compiling Foo ( test.hs, test.o )
test.hs:9:14: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.4.1 for x86_64-unknown-linux):
No skolem info:
[a_aD2[sk:2]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2945:5 in ghc:TcErrors
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
This panics on both GHC 8.2.2 and 8.4.1.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.4.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Panic when using StaticPointers with typed holes","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Adding a type hole when there is a type variable in `StaticPtr` throws a GHC panic:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE StaticPointers #-}\r\n\r\nmodule Foo where\r\n\r\nimport Data.Typeable\r\nimport GHC.StaticPtr\r\n\r\nfoo :: Typeable a => StaticPtr a\r\nfoo = static _ \r\n}}}\r\n\r\n{{{\r\n\r\n[1 of 1] Compiling Foo ( test.hs, test.o )\r\n\r\ntest.hs:9:14: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.4.1 for x86_64-unknown-linux):\r\n\tNo skolem info:\r\n [a_aD2[sk:2]]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcErrors.hs:2945:5 in ghc:TcErrors\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\n\r\nThis panics on both GHC 8.2.2 and 8.4.1.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15007Don't keep shadowed variables in ghci, both renamer and type checker2021-10-07T13:16:12ZTao Hesighingnow@gmail.comDon't keep shadowed variables in ghci, both renamer and type checkerIn #14052, we reverted [D2447](https://phabricator.haskell.org/D2447), then #11547 exists in HEAD again. In [ticket:14052\#comment:151549](https://gitlab.haskell.org//ghc/ghc/issues/14052#note_151549) and [ticket:14052\#comment:140478](h...In #14052, we reverted [D2447](https://phabricator.haskell.org/D2447), then #11547 exists in HEAD again. In [ticket:14052\#comment:151549](https://gitlab.haskell.org//ghc/ghc/issues/14052#note_151549) and [ticket:14052\#comment:140478](https://gitlab.haskell.org//ghc/ghc/issues/14052#note_140478), we decide that shadowed variables shouldn't be keep at all. This ticket is created to track the idea.
The same error of #11547 was also reported in [ticket:14996\#comment:151477](https://gitlab.haskell.org//ghc/ghc/issues/14996#note_151477),
> ```
> $ inplace/bin/ghc-stage2 --interactive
> GHCi, version 8.5.20180403: http://www.haskell.org/ghc/ :? for help
> Prelude> 1
> 1
> Prelude> 1
> 1
> Prelude> _
>
> <interactive>:1:1: error:
> GHC internal error: ‘Ghci1.it’ is not in scope during type > checking, but it passed the renamer
> tcl_env of environment: []
> ```
>
> (giving "1" twice is needed to reproduce the error)
NB: input "1" twice to create shadowed context is necessary to reproduce this bug.8.6.1Tao Hesighingnow@gmail.comTao Hesighingnow@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/14996Typed holes are very slow2019-07-07T18:14:45ZSimon Peyton JonesTyped holes are very slowIf you type at the GHCi prompt
```
ghci> 3 _ 4
```
(which I did for #14969), you get a multi-second pause before the error message comes out.
I think this is because the error-message generator is looking through the entire type envir...If you type at the GHCi prompt
```
ghci> 3 _ 4
```
(which I did for #14969), you get a multi-second pause before the error message comes out.
I think this is because the error-message generator is looking through the entire type environment. But it's really too slow.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.2.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Typed holes are very slow","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If you type at the GHCi prompt\r\n{{{\r\nghci> 3 _ 4\r\n}}}\r\n(which I did for #14969), you get a multi-second pause before the error message comes out.\r\n\r\nI think this is because the error-message generator is looking through the entire type environment. But it's really too slow.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14969Underconstrained typed holes are non-performant2019-07-07T18:14:51ZjohnleoUnderconstrained typed holes are non-performantWith a fresh build of 8.5:
```
GHCi, version 8.5.20180323: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /Users/leo/.ghci
Prelude> 3 _ 4
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.5.2018032...With a fresh build of 8.5:
```
GHCi, version 8.5.20180323: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /Users/leo/.ghci
Prelude> 3 _ 4
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.5.20180323 for x86_64-apple-darwin):
ASSERT failed!
2
1
t_a4j6[tau:1]
Maybe a_a4j7[tau:2]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1157:37 in ghc:Outputable
pprPanic, called at compiler/utils/Outputable.hs:1213:5 in ghc:Outputable
assertPprPanic, called at compiler/typecheck/TcMType.hs:720:54 in ghc:TcMType
```
I believe this fails in earlier versions as well, but I haven't tested it.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.5 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"panic on incorrect syntax","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"With a fresh build of 8.5:\r\n{{{\r\nGHCi, version 8.5.20180323: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /Users/leo/.ghci\r\nPrelude> 3 _ 4\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.5.20180323 for x86_64-apple-darwin):\r\n\tASSERT failed!\r\n 2\r\n 1\r\n t_a4j6[tau:1]\r\n Maybe a_a4j7[tau:2]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1157:37 in ghc:Outputable\r\n pprPanic, called at compiler/utils/Outputable.hs:1213:5 in ghc:Outputable\r\n assertPprPanic, called at compiler/typecheck/TcMType.hs:720:54 in ghc:TcMType\r\n}}}\r\n\r\nI believe this fails in earlier versions as well, but I haven't tested it.\r\n\r\n","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/14884Type holes cause assertion failure in ghc-stage2 compiler during type checking2019-07-07T18:15:11ZTao Hesighingnow@gmail.comType holes cause assertion failure in ghc-stage2 compiler during type checkingghc-stage2 panic! due to assertion failure when compiling the following code with `ghc-stage2 Bug.hs`
```hs
module Bug where
x :: IO ()
x = _ print "abc"
```
Callstack:
```
λ inplace\bin\ghc-stage2 Bug.hs
[1 of 1] Compiling Bug ...ghc-stage2 panic! due to assertion failure when compiling the following code with `ghc-stage2 Bug.hs`
```hs
module Bug where
x :: IO ()
x = _ print "abc"
```
Callstack:
```
λ inplace\bin\ghc-stage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.5.20180225 for x86_64-unknown-mingw32):
ASSERT failed!
t_a4ec[tau:2]
2
1
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler\utils\Outputable.hs:1150:37 in ghc:Outputable
pprPanic, called at compiler\utils\Outputable.hs:1206:5 in ghc:Outputable
assertPprPanic, called at compiler\\typecheck\\TcType.hs:1187:83 in ghc:TcType
CallStack (from -prof):
TcInteract.solve_loop (compiler\typecheck\TcInteract.hs:(247,9)-(254,44))
TcInteract.solveSimples (compiler\typecheck\TcInteract.hs:(241,5)-(243,21))
TcRnDriver.simplifyTop (compiler\typecheck\TcRnDriver.hs:408:25-39)
TcRnDriver.tcRnSrcDecls (compiler\typecheck\TcRnDriver.hs:254:25-65)
```
The failed assertion is `checkTcLevelInvariant ctxt_tclvl tv_tclvl` in `isTouchableMetaTyVar`:
```hs
isTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool
isTouchableMetaTyVar ctxt_tclvl tv
| isTyVar tv -- See Note [Coercion variables in free variable lists]
= ASSERT2( tcIsTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv { mtv_tclvl = tv_tclvl }
-> ASSERT2( checkTcLevelInvariant ctxt_tclvl tv_tclvl,
ppr tv $$ ppr tv_tclvl $$ ppr ctxt_tclvl )
tv_tclvl `sameDepthAs` ctxt_tclvl
_ -> False
| otherwise = False
```
Notice that the ghc-stage1 compiler doesn't panic and report the type hole correctly. This seems a regression and I have checked that ghc-8.2.2 also works well.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Type holes cause assertion failure in ghc-stage2 compiler during type checking","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"ghc-stage2 panic! due to assertion failure when compiling the following code with `ghc-stage2 Bug.hs`\r\n\r\n{{{#!hs\r\nmodule Bug where\r\n\r\nx :: IO ()\r\nx = _ print \"abc\"\r\n}}}\r\n\r\nCallstack:\r\n\r\n{{{\r\nλ inplace\\bin\\ghc-stage2 Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.5.20180225 for x86_64-unknown-mingw32):\r\n ASSERT failed!\r\n t_a4ec[tau:2]\r\n 2\r\n 1\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler\\utils\\Outputable.hs:1150:37 in ghc:Outputable\r\n pprPanic, called at compiler\\utils\\Outputable.hs:1206:5 in ghc:Outputable\r\n assertPprPanic, called at compiler\\\\typecheck\\\\TcType.hs:1187:83 in ghc:TcType\r\nCallStack (from -prof):\r\n TcInteract.solve_loop (compiler\\typecheck\\TcInteract.hs:(247,9)-(254,44))\r\n TcInteract.solveSimples (compiler\\typecheck\\TcInteract.hs:(241,5)-(243,21))\r\n TcRnDriver.simplifyTop (compiler\\typecheck\\TcRnDriver.hs:408:25-39)\r\n TcRnDriver.tcRnSrcDecls (compiler\\typecheck\\TcRnDriver.hs:254:25-65)\r\n}}}\r\n\r\nThe failed assertion is `checkTcLevelInvariant ctxt_tclvl tv_tclvl` in `isTouchableMetaTyVar`:\r\n\r\n{{{#!hs\r\nisTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool\r\nisTouchableMetaTyVar ctxt_tclvl tv\r\n | isTyVar tv -- See Note [Coercion variables in free variable lists]\r\n = ASSERT2( tcIsTcTyVar tv, ppr tv )\r\n case tcTyVarDetails tv of\r\n MetaTv { mtv_tclvl = tv_tclvl }\r\n -> ASSERT2( checkTcLevelInvariant ctxt_tclvl tv_tclvl,\r\n ppr tv $$ ppr tv_tclvl $$ ppr ctxt_tclvl )\r\n tv_tclvl `sameDepthAs` ctxt_tclvl\r\n _ -> False\r\n | otherwise = False\r\n}}}\r\n\r\nNotice that the ghc-stage1 compiler doesn't panic and report the type hole correctly. This seems a regression and I have checked that ghc-8.2.2 also works well.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14858Typed hole subtitution search fails in the REPL2019-07-07T18:15:18Zpaf31Typed hole subtitution search fails in the REPLIt seems as though type class defaulting might be happening before the search.
This finds only undefined:
`
> _traverse print "abc"
<interactive>:20:1: error:
• Found hole: _traverse :: (() -> IO ()) -> [Char] -> t
Where: ‘...It seems as though type class defaulting might be happening before the search.
This finds only undefined:
`
> _traverse print "abc"
<interactive>:20:1: error:
• Found hole: _traverse :: (() -> IO ()) -> [Char] -> t
Where: ‘t’ is a rigid type variable bound by
the inferred type of it :: t
at <interactive>:20:1-21
Or perhaps ‘_traverse’ is mis-spelled, or not in scope
• In the expression: _traverse
In the expression: _traverse print "abc"
In an equation for ‘it’: it = _traverse print "abc"
• Relevant bindings include it :: t (bound at <interactive>:20:1)
Valid substitutions include
undefined :: forall (a :: TYPE r).
GHC.Stack.Types.HasCallStack =>
a
(imported from ‘Prelude’ (and originally defined in ‘GHC.Err’))
`
Annotating the return type helps, but we still don't find traverse_:
`
> _traverse print "abc" :: IO ()
<interactive>:22:1: error:
• Found hole: _traverse :: (() -> IO ()) -> [Char] -> IO ()
Or perhaps ‘_traverse’ is mis-spelled, or not in scope
• In the expression: _traverse
In the expression: _traverse print "abc" :: IO ()
In an equation for ‘it’: it = _traverse print "abc" :: IO ()
• Relevant bindings include
it :: IO () (bound at <interactive>:22:1)
Valid substitutions include
mempty :: forall a. Monoid a => a
(imported from ‘Prelude’ (and originally defined in ‘GHC.Base’))
undefined :: forall (a :: TYPE r).
GHC.Stack.Types.HasCallStack =>
a
(imported from ‘Prelude’ (and originally defined in ‘GHC.Err’))
`
(note how print seems to have been defaulted to ())
Annotating the type of print helps:
`
> _traverse (print :: Char -> IO ()) "abc" :: IO ()
<interactive>:23:1: error:
• Found hole: _traverse :: (Char -> IO ()) -> [Char] -> IO ()
Or perhaps ‘_traverse’ is mis-spelled, or not in scope
• In the expression: _traverse
In the expression:
_traverse (print :: Char -> IO ()) "abc" :: IO ()
In an equation for ‘it’:
it = _traverse (print :: Char -> IO ()) "abc" :: IO ()
• Relevant bindings include
it :: IO () (bound at <interactive>:23:1)
Valid substitutions include
mempty :: forall a. Monoid a => a
(imported from ‘Prelude’ (and originally defined in ‘GHC.Base’))
undefined :: forall (a :: TYPE r).
GHC.Stack.Types.HasCallStack =>
a
(imported from ‘Prelude’ (and originally defined in ‘GHC.Err’))
foldMap :: forall (t :: * -> *).
Foldable t =>
forall m a. Monoid m => (a -> m) -> t a -> m
(imported from ‘Prelude’
(and originally defined in ‘Data.Foldable’))
mapM_ :: forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
(imported from ‘Prelude’
(and originally defined in ‘Data.Foldable’))
traverse_ :: forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
(imported from ‘Data.Foldable’)
`
This was found with 8.4.1-rc.1.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.4.1-alpha3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Typed hole subtitution search fails in the REPL","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1-alpha3","keywords":["holes","substitutions","typed"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"It seems as though type class defaulting might be happening before the search.\r\n\r\nThis finds only undefined:\r\n\r\n {{{#!text\r\n> _traverse print \"abc\"\r\n\r\n<interactive>:20:1: error:\r\n • Found hole: _traverse :: (() -> IO ()) -> [Char] -> t\r\n Where: ‘t’ is a rigid type variable bound by\r\n the inferred type of it :: t\r\n at <interactive>:20:1-21\r\n Or perhaps ‘_traverse’ is mis-spelled, or not in scope\r\n • In the expression: _traverse\r\n In the expression: _traverse print \"abc\"\r\n In an equation for ‘it’: it = _traverse print \"abc\"\r\n • Relevant bindings include it :: t (bound at <interactive>:20:1)\r\n Valid substitutions include\r\n undefined :: forall (a :: TYPE r).\r\n GHC.Stack.Types.HasCallStack =>\r\n a\r\n (imported from ‘Prelude’ (and originally defined in ‘GHC.Err’))\r\n }}}\r\n\r\nAnnotating the return type helps, but we still don't find traverse_:\r\n\r\n {{{#!text\r\n> _traverse print \"abc\" :: IO ()\r\n\r\n<interactive>:22:1: error:\r\n • Found hole: _traverse :: (() -> IO ()) -> [Char] -> IO ()\r\n Or perhaps ‘_traverse’ is mis-spelled, or not in scope\r\n • In the expression: _traverse\r\n In the expression: _traverse print \"abc\" :: IO ()\r\n In an equation for ‘it’: it = _traverse print \"abc\" :: IO ()\r\n • Relevant bindings include\r\n it :: IO () (bound at <interactive>:22:1)\r\n Valid substitutions include\r\n mempty :: forall a. Monoid a => a\r\n (imported from ‘Prelude’ (and originally defined in ‘GHC.Base’))\r\n undefined :: forall (a :: TYPE r).\r\n GHC.Stack.Types.HasCallStack =>\r\n a\r\n (imported from ‘Prelude’ (and originally defined in ‘GHC.Err’))\r\n }}}\r\n\r\n(note how print seems to have been defaulted to ())\r\n\r\nAnnotating the type of print helps:\r\n\r\n {{{#!text\r\n> _traverse (print :: Char -> IO ()) \"abc\" :: IO ()\r\n\r\n<interactive>:23:1: error:\r\n • Found hole: _traverse :: (Char -> IO ()) -> [Char] -> IO ()\r\n Or perhaps ‘_traverse’ is mis-spelled, or not in scope\r\n • In the expression: _traverse\r\n In the expression:\r\n _traverse (print :: Char -> IO ()) \"abc\" :: IO ()\r\n In an equation for ‘it’:\r\n it = _traverse (print :: Char -> IO ()) \"abc\" :: IO ()\r\n • Relevant bindings include\r\n it :: IO () (bound at <interactive>:23:1)\r\n Valid substitutions include\r\n mempty :: forall a. Monoid a => a\r\n (imported from ‘Prelude’ (and originally defined in ‘GHC.Base’))\r\n undefined :: forall (a :: TYPE r).\r\n GHC.Stack.Types.HasCallStack =>\r\n a\r\n (imported from ‘Prelude’ (and originally defined in ‘GHC.Err’))\r\n foldMap :: forall (t :: * -> *).\r\n Foldable t =>\r\n forall m a. Monoid m => (a -> m) -> t a -> m\r\n (imported from ‘Prelude’\r\n (and originally defined in ‘Data.Foldable’))\r\n mapM_ :: forall (t :: * -> *) (m :: * -> *) a b.\r\n (Foldable t, Monad m) =>\r\n (a -> m b) -> t a -> m ()\r\n (imported from ‘Prelude’\r\n (and originally defined in ‘Data.Foldable’))\r\n traverse_ :: forall (t :: * -> *) (f :: * -> *) a b.\r\n (Foldable t, Applicative f) =>\r\n (a -> f b) -> t a -> f ()\r\n (imported from ‘Data.Foldable’)\r\n }}}\r\n\r\nThis was found with 8.4.1-rc.1.","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1Tao Hesighingnow@gmail.comTao Hesighingnow@gmail.com