Cannot sign an expression with its inferred type (or any type at all).
Summary
I have designed a polymorphic expression that GHC can infer the type of, but cannot type even with that very type. I have evidence that the computation expressed by this expression does work. I asked around but no one has come forward with an explanation of the issue so far. Halp.
Steps to reproduce
- Get the code by this link. At this time I do not have a smaller example.
- Load it in
ghci
. - Check out
:type deasilsB . deasilsA
. - Try
deasils = deasilsB . deasilsA
.
Expected behavior
deasils
is assigned the expression deasilsB . deasilsA
with the type as inferred. Or else, the assignment is accepted with the type signature such as in the definition found commented out in the source code.
Actual behaviour
See long error.
% ghci-9.2.2 Squeeze.hs
GHCi, version 9.2.2: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/kindaro/code/dotfiles/ghci.conf
[1 of 1] Compiling Main ( Squeeze.hs, interpreted )
Ok, one module loaded.
λ :reload
[1 of 1] Compiling Main ( Squeeze.hs, interpreted )
Ok, one module loaded.
λ :type deasilsB . deasilsA
deasilsB . deasilsA
:: (ForAll peels Functor,
Squeezy'
seed
(Dress seed peels)
peels
(Strip seed (Dress seed peels) == '[]),
Squeezy'
(seed, value)
(Dress (seed, value) peels)
peels
(Strip (seed, value) (Dress (seed, value) peels) == '[])) =>
(Dress seed peels, value) -> Dress (seed, value) peels
λ deasils = deasilsB . deasilsA
<interactive>:3:1: error:
• Could not deduce: Dress seed0 peels0 ~ Dress seed peels
from the context: (ForAll peels Functor,
Squeezy'
seed
(Dress seed peels)
peels
(Strip seed (Dress seed peels) == '[]),
Squeezy'
(seed, value)
(Dress (seed, value) peels)
peels
(Strip (seed, value) (Dress (seed, value) peels) == '[]))
bound by the inferred type for ‘deasils’:
forall {peels :: [* -> *]} {seed} {value}.
(ForAll peels Functor,
Squeezy'
seed
(Dress seed peels)
peels
(Strip seed (Dress seed peels) == '[]),
Squeezy'
(seed, value)
(Dress (seed, value) peels)
peels
(Strip (seed, value) (Dress (seed, value) peels) == '[])) =>
(Dress seed peels, value) -> Dress (seed, value) peels
at <interactive>:3:1-29
Expected: (Dress seed peels, value) -> Dress (seed, value) peels
Actual: (Dress seed0 peels0, value)
-> Dress (seed0, value) peels0
NB: ‘Dress’ is a non-injective type family
The type variables ‘seed0’, ‘peels0’ are ambiguous
• In the ambiguity check for the inferred type for ‘deasils’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
When checking the inferred type
deasils :: forall {peels :: [* -> *]} {seed} {value}.
(ForAll peels Functor,
Squeezy'
seed
(Dress seed peels)
peels
(Strip seed (Dress seed peels) == '[]),
Squeezy'
(seed, value)
(Dress (seed, value) peels)
peels
(Strip (seed, value) (Dress (seed, value) peels) == '[])) =>
(Dress seed peels, value) -> Dress (seed, value) peels
Environment
- GHC version used: 8.10.7, 9.2.2.