Commutativity of Coercible sometimes doesn't work with QuantifiedConstraints
It seems that there is a surprising interaction between the coercible constraint solver and quantified constraints. Here's some code with some explanation in the comments:
{-# LANGUAGE QuantifiedConstraints #-}
import Data.Coerce
-- I think this should compile, but it doesn't.
--
-- I'd expect the quantified constraint to be instantiated to
-- (Coercible (f b) b), and via commutativity of Coercible, imply
-- (Coercible b (f b))
compileError0 :: forall f b. (forall a. Coercible (f a) a) => b -> f b
compileError0 = coerce
-- The fact that this compiles demonstrates that quantified
-- constraints is needed to demonstrate the issue.
compiles0 :: forall f b. Coercible (f b) b => b -> f b
compiles0 = coerce
-- Instantiation as (Coercible (f b) b) works fine.
compiles1 :: forall f b. (forall a. Coercible (f a) a) => f b -> b
compiles1 = coerce
-- Instantiation of (forall a. Coercible a (f a)) as
-- (Coercible b (f b)) works.
compiles2 :: forall f b. (forall a. Coercible a (f a)) => b -> f b
compiles2 = coerce
-- This is curious! It turns out that instantiation of
-- (forall a. Coercible a (f a)) does indeed get combined with
-- commutativity to imply (Coercible (f b) b)
compiles3 :: forall f b. (forall a. Coercible a (f a)) => f b -> b
compiles3 = coerce
I get the following error with both GHC-8.6.4
and also GHC built from recent source, 8.9.20190304
:
qc.hs:10:17: error:
• Couldn't match representation of type ‘b’ with that of ‘f b’
arising from a use of ‘coerce’
‘b’ is a rigid type variable bound by
the type signature for:
compileError0 :: forall (f :: * -> *) b.
(forall a. Coercible (f a) a) =>
b -> f b
at qc.hs:9:1-70
• In the expression: coerce
In an equation for ‘compileError0’: compileError0 = coerce
• Relevant bindings include
compileError0 :: b -> f b (bound at qc.hs:10:1)
|
10 | compileError0 = coerce