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/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/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/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/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.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/11186Give strong preference to type variable names in scope when reporting hole co...2019-07-07T18:31:35ZDavid FeuerGive strong preference to type variable names in scope when reporting hole contextsWhen using `ScopedTypeVariables` with typed holes, I want GHC to bend over backwards to preserve the names of type variables that the user has chosen to bring into scope. I can't immediately reproduce the situations I've run into recentl...When using `ScopedTypeVariables` with typed holes, I want GHC to bend over backwards to preserve the names of type variables that the user has chosen to bring into scope. I can't immediately reproduce the situations I've run into recently where that hasn't happened, but sometimes I've had a signature like
```hs
foo :: forall bar . ...
foo = ... _ ...
```
and yet the typed hole message shows that `bar` has been lost in unification and replaced by some unrelated name. I would very much prefer if this never happened.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.2 |
| Type | FeatureRequest |
| 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":"Give strong preference to type variable names in scope when reporting hole contexts","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.2","keywords":["typed-holes"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"When using `ScopedTypeVariables` with typed holes, I want GHC to bend over backwards to preserve the names of type variables that the user has chosen to bring into scope. I can't immediately reproduce the situations I've run into recently where that hasn't happened, but sometimes I've had a signature like\r\n\r\n{{{#!hs\r\nfoo :: forall bar . ...\r\nfoo = ... _ ...\r\n}}}\r\n\r\nand yet the typed hole message shows that `bar` has been lost in unification and replaced by some unrelated name. I would very much prefer if this never happened.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/10875Unexpected defaulting of partial type signatures and inconsistent behaviour w...2019-07-07T18:33:20ZholzenspUnexpected defaulting of partial type signatures and inconsistent behaviour when -fdefer-typed-holes is set.Maybe this should be one bug report and one feature request, but for now, I'll report them together. Consider the following program:
```hs
{-#LANGUAGE PartialTypeSignatures #-}
{-#LANGUAGE NamedWildCards #-}
{-#LANGUAGE NoMonomorphismRe...Maybe this should be one bug report and one feature request, but for now, I'll report them together. Consider the following program:
```hs
{-#LANGUAGE PartialTypeSignatures #-}
{-#LANGUAGE NamedWildCards #-}
{-#LANGUAGE NoMonomorphismRestriction #-}
foo :: _ => _outer
foo x = round $ (undefined::_inner) (1 + x)
```
This produces the following output in GHCi:
```
Foo.hs:5:8: Warning:
Found hole ‘_’ with inferred constraints: (Integral b, Num a)
In the type signature for ‘foo’: _ => _outer
Foo.hs:5:13: Warning:
Found hole ‘_outer’ with type: a -> b
Where: ‘b’ is a rigid type variable bound by
the inferred type of foo :: (Integral b, Num a) => a -> b
at Foo.hs:6:1
‘a’ is a rigid type variable bound by
the inferred type of foo :: (Integral b, Num a) => a -> b
at Foo.hs:6:1
In the type signature for ‘foo’: _ => _outer
Foo.hs:6:29: Warning:
Found hole ‘_inner’ with type: a -> Double
Where: ‘a’ is a rigid type variable bound by
the inferred type of foo :: (Integral b, Num a) => a -> b
at Foo.hs:6:1
Relevant bindings include
x :: a (bound at Foo.hs:6:5)
foo :: a -> b (bound at Foo.hs:6:1)
In an expression type signature: _inner
In the expression: undefined :: _inner
In the second argument of ‘($)’, namely
‘(undefined :: _inner) (1 + x)’
Ok, modules loaded: Main.
```
The inferred constraints for `_` (which I can't give a name, unfortunately) and the type reported in place of `_outer` are exactly what I expected. The type for `_inner` surprises me. Okay, the type is ambiguous, so for anything as general as `undefined`, arguably, it would need to default to something.
Let's use a typed hole instead of `undefined`:
```hs
foo :: _ => _outer
foo x = round $ _hole (1 + x)
```
gives
```
Foo.hs:6:17:
Found hole ‘_hole’ with type: a -> Double
Where: ‘a’ is a rigid type variable bound by
the inferred type of foo :: a -> b at Foo.hs:6:1
Relevant bindings include
x :: a (bound at Foo.hs:6:5)
foo :: a -> b (bound at Foo.hs:6:1)
In the expression: _hole
In the second argument of ‘($)’, namely ‘_hole (1 + x)’
In the expression: round $ _hole (1 + x)
Failed, modules loaded: none.
```
Holy Guacamole, it still defaults to `Double`. I would consider this a bug, because GHC is telling me, that whatever I put there must result in a `Double`, which is too restrictive to be true. However, I seem to recall from the OutsideIn paper that there were some cases, even without GADTs, where principality was difficult. Was this one of them?
Moving on, I was actually trying to get all my holes typed for me in one compiler execution. GHC behaves according to spec; typed holes produce errors by default and when something breaks on an error, it doesn't produce the warnings for partial type signatures. Let's `-fdefer-typed-holes` and compile again:
```
Prelude> :set -fdefer-typed-holes
Prelude> :r
[1 of 1] Compiling Main ( Foo.hs, interpreted )
Foo.hs:5:8: Warning:
Found hole ‘_’ with inferred constraints: ()
In the type signature for ‘foo’: _ => _outer
Foo.hs:5:13: Warning:
Found hole ‘_outer’ with type: a -> b
Where: ‘b’ is a rigid type variable bound by
the inferred type of foo :: a -> b at Foo.hs:6:1
‘a’ is a rigid type variable bound by
the inferred type of foo :: a -> b at Foo.hs:6:1
In the type signature for ‘foo’: _ => _outer
Foo.hs:6:17: Warning:
Found hole ‘_hole’ with type: a -> Double
Where: ‘a’ is a rigid type variable bound by
the inferred type of foo :: a -> b at Foo.hs:6:1
Relevant bindings include
x :: a (bound at Foo.hs:6:5)
foo :: a -> b (bound at Foo.hs:6:1)
In the expression: _hole
In the second argument of ‘($)’, namely ‘_hole (1 + x)’
In the expression: round $ _hole (1 + x)
Ok, modules loaded: Main.
```
Surely, this must be wrong. Suddenly `()` is the inferred set of constraints and an unconstrained `a -> b` will do for `_outer`. I would argue that the `1 +` still demainds `Num a` and that `round` still requires an instance of `Integral b`, even if `round`'s `RealFrac` constraint is satisfied by `_hole` producing a `Double`.
As said, maybe the erroneous types reported when `-fdefer-typed-holes` are a separate issue from the type of `_hole` not being the principal type, but I'm unsure, so I reported them together.https://gitlab.haskell.org/ghc/ghc/-/issues/5910Holes with other constraints2024-01-22T12:03:56ZxnyhpsHoles with other constraintsHello. As can be seen on http://hackage.haskell.org/trac/ghc/wiki/Holes and http://www.haskell.org/pipermail/glasgow-haskell-users/2012-January/021670.html, we've been working on adding holes to GHC. I'm opening this ticket about a speci...Hello. As can be seen on http://hackage.haskell.org/trac/ghc/wiki/Holes and http://www.haskell.org/pipermail/glasgow-haskell-users/2012-January/021670.html, we've been working on adding holes to GHC. I'm opening this ticket about a specific problem I've been having, and I hope someone has a suggestion of how to do it correctly.
As holes work quite similarly to implicit parameters (see the wiki-page for a comparison), we started out in the same way as implicit parameters. Typechecking of a hole generates a constraint (a new type of constraint), and the constraint solver will try to find the right type for each hole. The difference is that hole constraints never show up in a type, but their type is printed separately. This currently works correctly for simple typechecking, but it has some problems when other constraints are generated too. A simple example:
```
test :: String
test = show _h
```
Here, the `_h` denotes a hole named "h". If this function is defined like this inside a module it will currently fail:
```
test2.hs:2:8:
No instance for (Show a0)
arising from a use of `show'
The type variable `a0' is ambiguous
Possible fix: add a type signature that fixes these type variable(s)
In the expression: show (_h)
In an equation for `test': test = show (_h)
Failed, modules loaded: none.
```
The problem is that the `Show` constraint is still there. If the type signature is omitted and the monomorphism restriction off, we can see that the types found are:
```
Found the following holes:
_h :: GHC.Show.Show a => a
...
test :: Show a => String
```
The problem is the `Show a` that is irrelevant to the actual type of `test`, but nevertheless it's there.
How do other approaches handle this?
**undefined**:
```
test :: String
test = show undefined
```
Gives the same ambiguity error, even if the signature is omitted.
**Implicit parameters**:
```
test = show ?h
```
This works, but generates the following type signature:
```
test :: (Show a, ?h::a) => String
```
So, as I'd want to use it, this is wrong. It has the right ingredients, but I'd want:
```
test :: (?h :: (Show a) => a) => String
```
For implicit parameters the difference doesn't matter too much, as implicit parameters are still parameters: they still show up in the type signature. A hole is not required to be a parameter, so it's more important that every constraint only shows up where it's necessary.
So the problem is that I don't know how to select from the constraints only those that are applicable to the expression/function itself, and those that apply to which of the holes. I've tried typechecking all of the holes first, but I don't know how to determine how to change the constraint set after that. If you need more information about how it currently works, or have any feedback on this approach, please let me know. I'm still quite unfamiliar with the architecture of GHC. :)
----
I'm attaching a patch against the master branch on git with my current work in case someone is interested in trying it. Note that the code generation is pretty much a stub and it will panic if you try to run a function with a hole. It will print the holes of an expression if you invoke `:t` (it doesn't currently print the holes when loading a module, but it should still print them with `:t` on a function from the module). Also, I do not recommend building stage 1 with this, as some packages have some issues. Easiest is to build stage 1 and the packages without these changes and then applying the patch and then building only stage 2.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.5 |
| Type | FeatureRequest |
| TypeOfFailure | IncorrectWarning |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Holes with other constraints","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.5","keywords":["holes"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Hello. As can be seen on http://hackage.haskell.org/trac/ghc/wiki/Holes and http://www.haskell.org/pipermail/glasgow-haskell-users/2012-January/021670.html, we've been working on adding holes to GHC. I'm opening this ticket about a specific problem I've been having, and I hope someone has a suggestion of how to do it correctly.\r\n\r\nAs holes work quite similarly to implicit parameters (see the wiki-page for a comparison), we started out in the same way as implicit parameters. Typechecking of a hole generates a constraint (a new type of constraint), and the constraint solver will try to find the right type for each hole. The difference is that hole constraints never show up in a type, but their type is printed separately. This currently works correctly for simple typechecking, but it has some problems when other constraints are generated too. A simple example:\r\n\r\n{{{\r\ntest :: String\r\ntest = show _h\r\n}}}\r\n\r\nHere, the {{{_h}}} denotes a hole named \"h\". If this function is defined like this inside a module it will currently fail:\r\n\r\n{{{\r\ntest2.hs:2:8:\r\n No instance for (Show a0)\r\n arising from a use of `show'\r\n The type variable `a0' is ambiguous\r\n Possible fix: add a type signature that fixes these type variable(s)\r\n In the expression: show (_h)\r\n In an equation for `test': test = show (_h)\r\nFailed, modules loaded: none.\r\n}}}\r\n\r\nThe problem is that the {{{Show}}} constraint is still there. If the type signature is omitted and the monomorphism restriction off, we can see that the types found are:\r\n\r\n{{{\r\nFound the following holes: \r\n_h :: GHC.Show.Show a => a\r\n...\r\ntest :: Show a => String\r\n}}}\r\n\r\nThe problem is the {{{Show a}}} that is irrelevant to the actual type of {{{test}}}, but nevertheless it's there.\r\n\r\n\r\nHow do other approaches handle this?\r\n\r\n'''undefined''':\r\n{{{\r\ntest :: String\r\ntest = show undefined\r\n}}}\r\n\r\nGives the same ambiguity error, even if the signature is omitted.\r\n\r\n'''Implicit parameters''':\r\n{{{\r\ntest = show ?h\r\n}}}\r\n\r\nThis works, but generates the following type signature:\r\n\r\n{{{\r\ntest :: (Show a, ?h::a) => String\r\n}}}\r\n\r\nSo, as I'd want to use it, this is wrong. It has the right ingredients, but I'd want:\r\n\r\n{{{\r\ntest :: (?h :: (Show a) => a) => String\r\n}}}\r\n\r\nFor implicit parameters the difference doesn't matter too much, as implicit parameters are still parameters: they still show up in the type signature. A hole is not required to be a parameter, so it's more important that every constraint only shows up where it's necessary.\r\n\r\nSo the problem is that I don't know how to select from the constraints only those that are applicable to the expression/function itself, and those that apply to which of the holes. I've tried typechecking all of the holes first, but I don't know how to determine how to change the constraint set after that. If you need more information about how it currently works, or have any feedback on this approach, please let me know. I'm still quite unfamiliar with the architecture of GHC. :)\r\n\r\n----\r\n\r\nI'm attaching a patch against the master branch on git with my current work in case someone is interested in trying it. Note that the code generation is pretty much a stub and it will panic if you try to run a function with a hole. It will print the holes of an expression if you invoke {{{:t}}} (it doesn't currently print the holes when loading a module, but it should still print them with {{{:t}}} on a function from the module). Also, I do not recommend building stage 1 with this, as some packages have some issues. Easiest is to build stage 1 and the packages without these changes and then applying the patch and then building only stage 2.","type_of_failure":"IncorrectWarning","blocking":[]} -->8.0.1