Strange polytype unification behavior
Summary
While looking into https://github.com/ghc-proposals/ghc-proposals/issues/558, I noticed some strangeness around can_eq_nc_forall
, which I thought I should record while it is fresh. Specifically:
Bug
- When there are nested
forall
s, we only check that the outermost visibilities match:- We (correctly) reject unifying
forall b -> (a, b)
withforall b. (a, b)
, but - we (wrongly) succeed unifying
forall a. forall b -> (a, b)
withforall a. forall b. (a, b)
.
- We (correctly) reject unifying
Opportuntity
- We only match successfully if the
forall
nesting depth is the same for both types. For nominal equality, this is expected (I think), but it's a bit odd for representational equality. If we havenewtype P a = PC (forall c. (a, c))
:- We (correctly?) representationally unify
P a
withforall b. (a, b)
, but - we reject representationally unifying
forall a. P a
withforall a. forall b. (a, b)
.
- We (correctly?) representationally unify
Here is a concrete example:
import Data.Coerce
newtype M = MkM (forall a b. a -> b -> b)
newtype N a = MkN (forall b. a -> b -> b)
newtype P = MkP (forall a. N a)
g1 :: M -> P
g1 x = coerce x
g2 :: P -> M
g2 x = coerce x
It is not unreasonable to expect g1
and g2
to typecheck; there are perfectly well-behaved coercions that connect them.
Expected behavior
- We should definitely reject matching
forall a. forall b -> (a, b)
withforall a. forall b. (a, b)
, at least when matching for nominal equality. - It's surprising and neat-o that representational equality solving with newtypes around polytypes even sort-of works. But I don't have an informed opinion about whether this "should" be expected to generally work.