Typed holes show applications to inferred arguments
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.
Edited by Krzysztof Gogolewski