GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2023-07-11T14:54:42Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/23611hole in type application: is accepted, but should give error, with informativ...2023-07-11T14:54:42Zjwaldmannhole in type application: is accepted, but should give error, with informative messageghci (9.6.2) is silent about holes in type applications:
```
ghci> (<>) @[ _ ] "foo" "bar"
"foobar"
```
while it prints the substitution for holes in types, and errs:
```
ghci> (<>) "foo" "bar" :: [ _ ]
<interactive>:12:24: error: [GH...ghci (9.6.2) is silent about holes in type applications:
```
ghci> (<>) @[ _ ] "foo" "bar"
"foobar"
```
while it prints the substitution for holes in types, and errs:
```
ghci> (<>) "foo" "bar" :: [ _ ]
<interactive>:12:24: error: [GHC-88464]
• Found type wildcard ‘_’ standing for ‘Char’
```sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://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/18878Scoped Typed Holes2020-11-09T08:52:14ZparsonsmattScoped Typed Holes## Motivation
Sometimes I know that a module defines a function, but I've forgotten the name. The concrete example is this:
```haskell
import Database.Persist.Sql as Sql
-- snip... lots of code
someFunc =<< _f userId
-- etc.....## Motivation
Sometimes I know that a module defines a function, but I've forgotten the name. The concrete example is this:
```haskell
import Database.Persist.Sql as Sql
-- snip... lots of code
someFunc =<< _f userId
-- etc...
```
The inferred type of `_f` is `UserId -> SqlPersistT m (Entity User)`. There are too many terms in scope and for whatever reason GHC does not suggest any valid hole fits.
But I know the function is in `Database.Persist.Sql`! So I ideally would be able to write:
```haskell
someFunc =<< Sql._f userId
```
Which should limit the *scope* of possible hole fits to those imported from `Database.Persist.Sql`. Right now, it just fails with an error message:
```
lumi-mojo> /home/matt/Projects/lumi/mojo/lib/Lumi/Database/API/Zendesk.hs:574:8: error:
lumi-mojo> Not in scope: ‘Sql._f’
lumi-mojo> Perhaps you meant one of these:
lumi-mojo> data constructor ‘Sql.Eq’ (imported from Database.Persist.Sql),
lumi-mojo> data constructor ‘Sql.Ge’ (imported from Database.Persist.Sql),
lumi-mojo> data constructor ‘Sql.Gt’ (imported from Database.Persist.Sql)
lumi-mojo> Module ‘Database.Persist.Sql’ does not export ‘_f’.
lumi-mojo> |
lumi-mojo> 574 | what = Sql._f
lumi-mojo> | ^^^^^^
lumi-mojo>
```
## Proposal
I'd like for `ModuleName._hole_expression` to go through the typed hole search if the term isn't exported from the module, limiting search to items exported from the module.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/18491Typed holes shouldn't cause linearity errors2021-04-30T14:35:05ZArnaud SpiwackTyped holes shouldn't cause linearity errors## Summary
Writing a typed hole with linear arguments in scope gives spurious linearity errors. It does not help that these errors are display first, so that in ghcid, for instance, we may not even be able see the type of the hole.
## ...## Summary
Writing a typed hole with linear arguments in scope gives spurious linearity errors. It does not help that these errors are display first, so that in ghcid, for instance, we may not even be able see the type of the hole.
## Steps to reproduce
```haskell
{-# LANGUAGE LinearTypes #-}
f :: Int #-> Bool #-> Char
f x y = _
```
Raises the following error:
```
<interactive>:15:31: error:
• Couldn't match type ‘'Many’ with ‘'One’
arising from multiplicity of ‘x’
• In an equation for ‘f’: f x y = _
<interactive>:15:33: error:
• Couldn't match type ‘'Many’ with ‘'One’
arising from multiplicity of ‘y’
• In an equation for ‘f’: f x y = _
<interactive>:15:37: error:
• Found hole: _ :: Char
• In the expression: _
In an equation for ‘f’: f x y = _
• Relevant bindings include
y :: Bool (bound at <interactive>:15:33)
x :: Int (bound at <interactive>:15:31)
f :: Int #-> Bool #-> Char (bound at <interactive>:15:29)
Valid hole fits include
maxBound :: forall a. Bounded a => a
with maxBound @Char
(imported from ‘Prelude’ (and originally defined in ‘GHC.Enum’))
minBound :: forall a. Bounded a => a
with minBound @Char
(imported from ‘Prelude’ (and originally defined in ‘GHC.Enum’))
```
Notice the two multiplicity errors at the top. Which are caused by the fact that the typechecker considers that `_` counts for 0 use of `x` and `y` (where it ought to be: an unknown number of uses).
## Expected behavior
Contrast the behaviour of `_` with the behaviour of an empty case:
```haskell
f :: Int #-> Bool #-> Char
f x y = () & \case {}
```
This compiles without a type error.
So holes should treat multiplicities exactly how a `case {}` would. After all, it's more or less the same idea: `_` uses `x` and `y` an unknown number of times, and `\case {}` consumes `x` and `y` an arbitrary number of times. Since we don't know how many `x`-s and `y`-s are in `_`, we don't want to complain about it, so it's natural to approximate `_` to be consuming `x` and `y` an arbitrary number of times.
## Environment
* GHC version used: current masterhttps://gitlab.haskell.org/ghc/ghc/-/issues/17773Typed holes panic: simplifyArgsWorker wandered into deeper water than usual2020-02-05T14:26:07ZRyan ScottTyped holes panic: simplifyArgsWorker wandered into deeper water than usualThe following code should not be expected to typecheck. But GHC does a fair bit worse and panics when it tries to typecheck it:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE...The following code should not be expected to typecheck. But GHC does a fair bit worse and panics when it tries to typecheck it:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import Data.Kind (Type)
import Data.Type.Equality ((:~:)(..))
import GHC.Generics (U1(..))
type family Sing :: k -> Type
data SU1 :: forall k (p :: k). U1 p -> Type where
SU1 :: SU1 'U1
type instance Sing = SU1
class PSAlternative (f :: Type -> Type) where
type (x :: f a) <|> (y :: f a) :: f a
type Empty :: f a
(%<|>) :: forall a (x :: f a) (y :: f a).
Sing x -> Sing y -> Sing (x <|> y)
sEmpty :: forall a. Sing (Empty :: f a)
class PSAlternative f => PSMonadPlus (f :: Type -> Type) where
type Mplus (x :: f a) (y :: f a) :: f a
type Mzero :: f a
sMplus :: forall a (x :: f a) (y :: f a).
Sing x -> Sing y -> Sing (Mplus x y)
sMzero :: forall a. Sing (Mzero :: f a)
instance PSAlternative U1 where
type x <|> y = 'U1
type Empty = 'U1
_ %<|> _ = SU1
sEmpty = SU1
instance PSMonadPlus U1 where
type Mplus x y = x <|> y
type Mzero = Empty
sMplus = (%<|>)
sMzero = sEmpty
class PSMonadPlus f => VMonadPlus f where
monadPlusMplus :: forall a (x :: f a) (y :: f a).
Sing x -> Sing y
-> Mzero x y :~: (x <|> y)
-- The mistake is above: it should actually be
-- -> Mplus x y :~: (x <|> y)
instance VMonadPlus U1 where
monadPlusMplus _ _ = _Refl
```
On GHC 8.8.2, the panic is:
```
$ /opt/ghc/8.8.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.8.2 for x86_64-unknown-linux):
simplifyArgsWorker wandered into deeper water than usual
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```
Older versions of GHC (dating back to 8.2.2) also panic on this program, although the exact message the panic prints out differs slightly between versions.https://gitlab.haskell.org/ghc/ghc/-/issues/16875Valid hole fits process is too slow to be enabled by default2022-01-25T12:36:33ZMatthew PickeringValid hole fits process is too slow to be enabled by defaultI am hearing anecdotal evidence that people are suggesting to turn on `-fno-valid-hole-fits` as typed holes causes compilation time to double (from 2s to 4s).
@trac\-isovector also reports
> i have a 140 line file with 17 modules impo...I am hearing anecdotal evidence that people are suggesting to turn on `-fno-valid-hole-fits` as typed holes causes compilation time to double (from 2s to 4s).
@trac\-isovector also reports
> i have a 140 line file with 17 modules imported: `doc <- fromJust <$> #getDomDocument page` transformed to `doc <- _ <$> #getDomDocument page` takes > 1 minute in ghci with the default settings
People just use `()` rather than `_` as `_` takes too long. I think we either have to make it more efficient or disable the feature by default.9.2.1Matthías Páll GissurarsonMatthías Páll Gissurarsonhttps://gitlab.haskell.org/ghc/ghc/-/issues/16781Some tests for valid hole fits are missing2019-07-08T11:15:04ZKrzysztof GogolewskiSome tests for valid hole fits are missingThe functionality of valid hole fits is not fully covered by tests.
I couldn't find any occurrence of `show-hole-matches-of-hole-fits`, `show-type-app-of-hole-fits`, `show-type-of-hole-fits`, `show-type-app-vars-of-hole-fits`, `show-pro...The functionality of valid hole fits is not fully covered by tests.
I couldn't find any occurrence of `show-hole-matches-of-hole-fits`, `show-type-app-of-hole-fits`, `show-type-of-hole-fits`, `show-type-app-vars-of-hole-fits`, `show-provenance-of-hole-fits`, `no-show-valid-hole-fits` in the `testsuite` directory. If I change TcHoleErrors
```
wrapDisp = ppWhen (has wrap && (sWrp || sWrpVars))
$ text "with" <+> if sWrp || not sTy
then occDisp <+> tyApp
- else tyAppVars
+ else text "foo"
```
then the testsuite passes.https://gitlab.haskell.org/ghc/ghc/-/issues/16456Typed holes show applications to inferred arguments2019-07-08T11:14:59ZKrzysztof GogolewskiTyped holes show applications to inferred argumentsTyped hole suggestions print type arguments using `@T`, even if the argument is inferred. For example,
```
λ> :set -XPolyKinds -XTypeApplications
λ> data T a = MkT
λ> foo :: T Int; foo = _
<interactive>:3:21: error:
• Found hole: _...Typed hole suggestions print type arguments using `@T`, even if the argument is inferred. For example,
```
λ> :set -XPolyKinds -XTypeApplications
λ> data T a = MkT
λ> foo :: T Int; foo = _
<interactive>:3:21: error:
• Found hole: _ :: T Int
• In the expression: _
In an equation for ‘foo’: foo = _
• Relevant bindings include
foo :: T Int (bound at <interactive>:3:15)
Valid hole fits include
foo :: T Int (bound at <interactive>:3:15)
MkT :: forall k (a :: k). T a
with MkT @* @Int
(defined at <interactive>:2:12)
```
The penultimate line should be `MkT @Int` (or, if we allowed to specify inferred arguments, something like `MkT @{*} @Int`).
The motivation comes from the linear types branch; in linear types, constructors have additional inferred multiplicity arguments, which significantly clutters the output.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/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/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.1