Implicit parameters can’t be polymorphic even if QuantifiedConstraints and ImpredicativeTypes are enabled; if this is intentional, it is poorly communicated
Summary
- GHC throws a parse error when
forallis used inside an implicit parameter constraint without explicit parentheses.x = ?y (1 :: Integer) x :: (?y::forall t. t -> t) => Integererror: parse error on input ‘forall’ - GHC refuses to narrow polymorphic implicit parameters.
x = ?y (1 :: Integer) x :: (?y::(forall t. t -> t)) => Integererror: • Couldn't match type: forall t. t -> t with: t0 -> Integer arising from a functional dependency between constraints: ‘?y::t0 -> Integer’ arising from a use of implicit parameter ‘?y’ at ‘?y::forall t. t -> t’ arising from the type signature for: x :: (?y::forall t. t -> t) => Integer at • In the expression: ?y In the expression: ?y 1 In an equation for ‘x’: x = ?y 1 - GHC unnecessarily specializes polymorphic implicit parameter declarations
let ?id = id in (?id 1, ?id True) :: (Integer, Bool)• Couldn't match type ‘Integer’ with ‘Bool’ arising from a functional dependency between constraints: ‘?id::Bool -> Bool’ arising from a use of implicit parameter ‘?id’ at ‘?id::Integer -> Integer’ arising from the implicit-parameter binding for ?id at • In the expression: ?id In the expression: ?id True In the expression: (?id 1, ?id True) :: (Integer, Bool) - GHC produces multiple undeclared implicit parameter errors for the same parameters if it is used as different types.
x = (?i (1 :: Integer), ?i (), ?i True)error: • Unbound implicit parameter (?i::Integer -> c) arising from a use of implicit parameter ‘?i’ • In the expression: ?i In the expression: ?i (1 :: Integer) In the expression: (?i (1 :: Integer), ?i (), ?i True) • Relevant bindings include x :: (c, c, c) (bound at) error: • Unbound implicit parameter (?i::() -> c) arising from a use of implicit parameter ‘?i’ • In the expression: ?i In the expression: ?i () In the expression: (?i (1 :: Integer), ?i (), ?i True) • Relevant bindings include x :: (c, c, c) (bound at) error: • Unbound implicit parameter (?i::Bool -> c) arising from a use of implicit parameter ‘?i’ • In the expression: ?i In the expression: ?i True In the expression: (?i (1 :: Integer), ?i (), ?i True) • Relevant bindings include x :: (c, c, c) (bound at) - All of these error messages do not make it clear that polymorphic implicit parameters aren’t supported.
In particular, the use of the term “functional dependency” makes this appear related to
-XFunctionalDependencies. Therefore: They should either be supported, or the error messages clarified.
Detailed explanation
When enabling the extensions ImplicitParams, QuantifiedConstraints & ImpredicativeTypes, one might expect implicit parameters to be able to carry polymorphic values. This is not the case.
Consider the following example:
example = (?const (), ?const True) --example: ?const = \_ -> ()Here, ?const is applied to two values of different types. If we replace the implicit parameter ?const with just const (), this would type-check fine:
example = (const () (), const () True) :: ((), ())However, GHC seems to infer the type of both uses of ?const separately:
ghci> example = (?const (), ?const True)
<interactive>:11:12: error:
• Unbound implicit parameter (?const::() -> b)
arising from a use of implicit parameter ‘?const’
• In the expression: ?const
In the expression: ?const ()
In the expression: (?const (), ?const True)
• Relevant bindings include
example :: (b, b) (bound at <interactive>:11:1)
<interactive>:11:23: error:
• Unbound implicit parameter (?const::Bool -> b)
arising from a use of implicit parameter ‘?const’
• In the expression: ?const
In the expression: ?const True
In the expression: (?const (), ?const True)
• Relevant bindings include
example :: (b, b) (bound at <interactive>:11:1)This seems like it could be fixed by explicitly typing the implicit parameter. However, unexpectedly, a first attempt at this may fail, since forall in an implicit parameter constraint is a syntax error unless surrounded by parentheses.
ghci> :{
ghci| example = (?const (), ?const True)
ghci| example :: (?const::forall t. t -> b) => (b, b)
ghci| :}
<interactive>:16:21: error: parse error on input ‘forall’Even after adding parentheses, you’ll find that GHC doesn’t attempt to properly match the polymorphic and monomorphic types:
ghci> { example = (?const (), ?const True); example :: (?const::(forall t. t -> b)) => (b, b) }
<interactive>:19:14: error:
• Couldn't match type: forall t. t -> b
with: () -> b
arising from a functional dependency between constraints:
‘?const::() -> b’
arising from a use of implicit parameter ‘?const’ at <interactive>:19:14-19
‘?const::forall t. t -> b’
arising from the type signature for:
example :: forall b.
(?const::forall t. t -> b) =>
(b, b) at <interactive>:19:39-87
• In the expression: ?const
In the expression: ?const ()
In the expression: (?const (), ?const True)
• Relevant bindings include
example :: (b, b) (bound at <interactive>:19:3)
<interactive>:19:25: error:
• Couldn't match type: forall t. t -> b
with: Bool -> b
arising from a functional dependency between constraints:
‘?const::Bool -> b’
arising from a use of implicit parameter ‘?const’ at <interactive>:19:25-30
‘?const::forall t. t -> b’
arising from the type signature for:
example :: forall b.
(?const::forall t. t -> b) =>
(b, b) at <interactive>:19:39-87
• In the expression: ?const
In the expression: ?const True
In the expression: (?const (), ?const True)
• Relevant bindings include
example :: (b, b) (bound at <interactive>:19:3)Inversely, GHC specializes too quickly when implicit parameters are bound.
ghci> let ?id = id in (?id 1, ?id True) :: (Integer, Bool)
<interactive>:20:25: error:
• Couldn't match type ‘Integer’ with ‘Bool’
arising from a functional dependency between constraints:
‘?id::Bool -> Bool’
arising from a use of implicit parameter ‘?id’ at <interactive>:20:25-27
‘?id::Integer -> Integer’
arising from the implicit-parameter binding for ?id at <interactive>:20:1-52
• In the expression: ?id
In the expression: ?id True
In the expression: (?id 1, ?id True) :: (Integer, Bool)One might attempt to solve this problem by placing the forall at the start of the implicit parameter constraint. This only defers the problem to the use site.
ghci> { example = (?const (), ?const True); example :: (forall t. ?const::t -> b) => (b, b) }
ghci> let ?const = \_ -> 1 :: Integer in example
<interactive>:25:36: error:
• Couldn't match type ‘p0’ with ‘t’
arising from a functional dependency between constraints:
‘?const::t -> Integer’
arising from a use of ‘example’ at <interactive>:25:36-42
‘?const::p0 -> Integer’
arising from the implicit-parameter binding for ?const at <interactive>:25:1-42
because type variable ‘t’ would escape its scope
This (rigid, skolem) type variable is bound by
a quantified context
at <interactive>:25:1-42
• In the expression: example
In the expression: let ?const = \ _ -> ... in example
In an equation for ‘it’: it = let ?const = \ _ -> ... in exampleEnvironment
- GHC version used: 9.2.1
Optional:
- Operating System: NixOS 22.05.20220107.ff377a7 (Quokka)
- GHC was a binary cache download used in a
nix shellenvironment, selected Nixpkgs attributehaskell.packages.ghc921.ghc
- GHC was a binary cache download used in a
- System Architecture:
Linux buggeryyacht-nixos 5.15.12 #1-NixOS SMP Wed Dec 29 11:29:03 UTC 2021 x86_64 GNU/Linux