Opened 12 months ago

Last modified 10 months ago

#15639 new bug

Surprising failure combining QuantifiedConstraints with Coercible

Reported by: dfeuer Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler (Type checker) Version: 8.5
Keywords: QuantifiedConstraints Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

I don't understand what's going wrong here.

-- Fishy.hs
{-# language RankNTypes, QuantifiedConstraints, RoleAnnotations #-}
module Fishy (Yeah, yeahCoercible) where
import Data.Coerce

data Yeah_ a = Yeah_ Int
newtype Yeah a = Yeah (Yeah_ a)
type role Yeah representational

yeahCoercible :: ((forall a b. Coercible (Yeah a) (Yeah b)) => r) -> r
yeahCoercible r = r


-- Fishy2.hs

module Fishy2 where

import Fishy
import Data.Type.Coercion
import Data.Coerce

yeah :: Coercion [Yeah a] [Yeah b]
yeah = yeahCoercible Coercion

I get

Fishy2.hs:8:22: error:
    • Couldn't match representation of type ‘a’ with that of ‘b’
        arising from a use of ‘Coercion’
      ‘a’ is a rigid type variable bound by
        the type signature for:
          yeah :: forall a b. Coercion [Yeah a] [Yeah b]
        at Fishy2.hs:7:1-34
      ‘b’ is a rigid type variable bound by
        the type signature for:
          yeah :: forall a b. Coercion [Yeah a] [Yeah b]
        at Fishy2.hs:7:1-34
    • In the first argument of ‘yeahCoercible’, namely ‘Coercion’
      In the expression: yeahCoercible Coercion
      In an equation for ‘yeah’: yeah = yeahCoercible Coercion
    • Relevant bindings include
        yeah :: Coercion [Yeah a] [Yeah b] (bound at Fishy2.hs:8:1)
  |
8 | yeah = yeahCoercible Coercion
  |

Change History (11)

comment:1 Changed 12 months ago by dfeuer

-ddump-cs-trace gives

Step 1[l:1,d:1] Kept as inert:
    [WD] hole{co_a11c} {1}:: t_ax2[tau:0]
                             GHC.Prim.~# 'GHC.Types.LiftedRep
simpl_loop iteration=0 (no new given superclasses = True, 1 simples to solve)
Step 2[l:0,d:1] Solved by unification:
    [WD] hole{co_a11c} {1}:: t_ax2[tau:0]
                             GHC.Prim.~# 'GHC.Types.LiftedRep
Constraint solver steps = 2
Step 1[l:2,d:0] Given forall-constraint:
    [G] df_a11t {0}:: forall a b. Coercible (Yeah a) (Yeah b)
Step 2[l:2,d:0] Decomposed TyConApp:
    [WD] hole{co_a11z} {0}:: Coercion a_a11w[tau:2] b_a11x[tau:2]
                             GHC.Prim.~# r_a11r[tau:1]
Step 3[l:2,d:0] Kept as inert:
    [WD] hole{co_a11F} {0}:: b_a11x[tau:2]
                             GHC.Prim.~# [Yeah b_a11l[sk:1]]
Kick out, tv = k_a11v[tau:2]
  n-kicked = 1
  kicked_out = WL {Eqs = [WD] hole{co_a11F} {0}:: b_a11x[tau:2]
                                                  GHC.Prim.~# [Yeah b_a11l[sk:1]] (CIrredCan(sol))}
  Residual inerts = {Given instances = [G] df_a11t {0}:: forall a b.
                                                         Coercible (Yeah a) (Yeah b)
                     Unsolved goals = 0}
Step 4[l:2,d:0] Solved by unification (1 kicked out):
    [D] _ {0}:: k_a11v[tau:2] GHC.Prim.~# *
Step 5[l:2,d:0] Solved by unification:
    [WD] hole{co_a11F} {0}:: b_a11x[tau:2]
                             GHC.Prim.~# [Yeah b_a11l[sk:1]]
Step 6[l:2,d:0] Solved by unification:
    [WD] hole{co_a11E} {0}:: a_a11w[tau:2]
                             GHC.Prim.~# [Yeah a_a11k[sk:1]]
Step 7[l:2,d:0] Solved by reflexivity:
    [WD] hole{co_a11D} {0}:: k_a11v[tau:2] GHC.Prim.~# *
Step 8[l:2,d:0] Dict/Top (solved wanted):
    [WD] $dCoercible_a11y {0}:: Coercible
                                  [Yeah a_a11k[sk:1]] [Yeah b_a11l[sk:1]]
Step 9[l:2,d:1] Decomposed TyConApp:
    [WD] hole{co_a11G} {1}:: [Yeah a_a11k[sk:1]]
                             ~R# [Yeah b_a11l[sk:1]]
Step 10[l:2,d:1] Decomposed TyConApp:
    [WD] hole{co_a11H} {1}:: Yeah a_a11k[sk:1] ~R# Yeah b_a11l[sk:1]
Step 11[l:2,d:1] Kept as inert:
    [WD] hole{co_a11I} {1}:: a_a11k[sk:1] ~R# b_a11l[sk:1]
Step 12[l:2,d:0] Given forall-constraint:
    [G] df_a11J {0}:: forall a b. Yeah a ~R# Yeah b
simpl_loop iteration=0 (no new given superclasses = False, 1 simples to solve)
Step 13[l:2,d:1] Kept as inert:
    [WD] hole{co_a11I} {1}:: a_a11k[sk:1] ~R# b_a11l[sk:1]
Constraint solver steps = 13

I don't know quite how to read this, but I'd have expected

Step 10[l:2,d:1] Decomposed TyConApp:
    [WD] hole{co_a11H} {1}:: Yeah a_a11k[sk:1] ~R# Yeah b_a11l[sk:1]

to interact with

Step 12[l:2,d:0] Given forall-constraint:
    [G] df_a11J {0}:: forall a b. Yeah a ~R# Yeah b

and resolve.

comment:2 Changed 12 months ago by dfeuer

Best guess: the solver doesn't check for relevant quantified constraints before reducing Yeah a_a11k[sk:1] ~R# Yeah b_a11l[sk:1] to a_a11k[sk:1] ~R# b_a11l[sk:1].

comment:3 Changed 12 months ago by dfeuer

Keywords: QuantifiedConstraints added

comment:4 Changed 12 months ago by dfeuer

If I had to guess, I would guess that there is no entirely satisfactory general solution to this problem. Given type role F representational (or type role F nominal) and forall a b. C a b => Coercible (F a) (F b), and seeking Coercible (F a) (F b) I very much doubt that there's a single optimal way to determine whether to reduce the wanted to C or to Coercible a b (or a ~ b). To be consistent with how this is handled for other classes, we "should" just reject the constraint altogether, as overlapping. But that would be sad, and I do suspect we can do better, at least for some special cases.

For example, if we're given forall a b. Coercible (F a) (F b), we want to think of that as improving the type role of F's parameter from whatever it may be to phantom. Similarly, if we're given forall a b. Coercible a b => Coercible (F a) (F b), we want to think of that as improving the type role of Fs parameter to representational, if it would otherwise be nominal. Adding such special cases to the constraint solver would certainly be a horribly ugly hack, but I don't really know what else we can do.

comment:5 Changed 12 months ago by simonpj

Can you explain more about this example? I think that it is important that

  • You give a role signature for Yeah. (What is the inferred signature?)
  • You export the type constructor for Yeah but not the data constructor.

But I'm a bit lost about what you expect to happen. Can you amplify? Why do you think it should typecheck? It'd probably help to give the declaration for Coercion too, for those of us who do not use it daily.

comment:6 Changed 10 months ago by malo

I'm having a similar issue using GHC 8.6.2. Posting as a comment on this ticket since I expect it's related. Here's a minimal example:

-- test.hs
{-# LANGUAGE RankNTypes, QuantifiedConstraints #-}

import Data.Coerce

data Foo i = Foo i
data Bar f i = Bar (f i)

-- When I ask that we can lift coercions through the functor...
class (forall i j. Coercible i j => Coercible (f i) (f j)) => MyFunctor f where
  -- ...

-- ...this works fine.
instance MyFunctor Foo

-- When I try to ask that we can lift coercions through a higher functor...
class (forall f g. (forall i. Coercible (f i) (g i)) => (forall i. Coercible (x f i) (x g i))) => MyHigherFunctor x where
 -- ...

-- ...this fails
instance MyHigherFunctor Bar

-- Output from ghci:
--
-- Prelude> :l test.hs
-- [1 of 1] Compiling Main             ( test.hs, interpreted )
--
-- test.hs:21:10: error:
--     • Couldn't match representation of type ‘f’ with that of ‘g’
--         arising from the superclasses of an instance declaration
--       ‘f’ is a rigid type variable bound by
--         a quantified context
--         at test.hs:1:1
--       ‘g’ is a rigid type variable bound by
--         a quantified context
--         at test.hs:1:1
--     • In the instance declaration for ‘MyHigherFunctor Bar’
--    |
-- 21 | instance MyHigherFunctor Bar
--    |          ^^^^^^^^^^^^^^^^^^^
-- Failed, no modules loaded.

Last edited 10 months ago by malo (previous) (diff)

comment:7 in reply to:  5 Changed 10 months ago by dfeuer

Replying to simonpj:

Can you explain more about this example? I think that it is important that

  • You give a role signature for Yeah. (What is the inferred signature?)

The inferred signature is type role Yeah phantom

  • You export the type constructor for Yeah but not the data constructor.

Yes. The export isn't really as relevant as the import it enables; when a newtype constructor is in scope that changes the coercion axioms the type checker uses for the type.

But I'm a bit lost about what you expect to happen. Can you amplify? Why do you think it should typecheck? It'd probably help to give the declaration for Coercion too, for those of us who do not use it daily.

The declaration of Coercion is

data Coercion a b where
  Coercion :: Coercible a b => Coercion a b

The situation is

yeahCoercible :: ((forall a b. Coercible (Yeah a) (Yeah b)) => r) -> r
yeahCoercible r = r

-- Fishy2.hs

yeah :: Coercion [Yeah a] [Yeah b]
yeah = yeahCoercible Coercion

We call yeahCoercible with Coercion. For this to typecheck, we need

Coercion :: (forall a b. Coercible (Yeah a) (Yeah b)) => Coercion [Yeah a] [Yeah b]

Put another way, we need Coercible (Yeah a) (Yeah b) to imply Coercible [Yeah a] [Yeah b]. Under normal circumstances, that would follow from the fact that []'s parameter has a representational role. But the constraint solver isn't figuring that out.

comment:8 Changed 10 months ago by dfeuer

Let's go through this according to the user's guide:

In the light of the overlap decision, instance lookup works like this when trying to solve a class constraint C t

  1. First see if there is a given un-quantified constraint C t. If so, use it to solve the constraint.
  2. If not, look at all the available given quantified constraints; if exactly one one matches C t, choose it; if more than one matches, report an error.
  3. If no quantified constraints match, look up in the global instances, as described in ...

When type checking the use of the Coercion constructor in yeah, we want Coercible [Yeah a] [Yeah b]. There are no given constraints (quantified or otherwise) matching that, so we use the global instance Coercible x y => Coercible [x] [y], producing the wanted Coercible (Yeah a) (Yeah b). We have no matching unquantified givens, so we look for quantified givens. We (should) have a match: forall a b. Coercible (Yeah a) (Yeah b), which should solve the wanted. However, it appears that GHC is instead choosing the global instance forall a b. Coercible a b => Coercible (Yeah a) (Yeah b), leading to an unsatisfiable Coercible a b.

So I don't think the current behavior matches the user's guide.

comment:9 Changed 10 months ago by dfeuer

malo, I don't think the problem you're encountering is related at all. You're hoping that forall i. Coercible (f i) (g i) will satisfy the type role Bar representational nominal requirement. But we don't have such an extensionality rule. Perhaps we could add one somehow, but that would be quite independent.

comment:10 Changed 10 months ago by simonpj

So I don't think the current behavior matches the user's guide.

That's probably true. The built-in rules for Coercible apply first. So we reduce Coercible (Yeah a) (Yeah b) to Coercible a (Yeah b) and thence to Coercible a b. All this before we even start to consider instances.

It's a bit like type-class overlap. GHC doesn't have backtracking, and just picks one path. If you have overlap (as here, in this case between a quantified constraint and a built-in equality-decomposition rule) then GHC just picks one (in this case the built-in rule).

The best thing is to avoid overlap.

comment:11 in reply to:  10 Changed 10 months ago by dfeuer

Replying to simonpj:

The best thing is to avoid overlap.

This is a very good general principle (and the reason I was concerned about bundling implication constraints with quantified constraints). But I think the special case of Coercible deserves some special consideration.

Overlap is very often (perhaps usually) unavoidable when using quantified constraints with Coercible. There's just no way to hide the global mechanism. So I think it pays to consider how we can refine the overlap rules to make these constraints as useful as possible. I conjecture that we will get strictly or almost strictly better results by applying quantified constraints before and between built-in rules (other than symmetry, which I imagine does some global canonicalization). We seem to already do something special to allow things to work as expected when pattern matching on Coercions to locally reveal Coercible instances. Can we do something similar for quantified constraints?

Note: See TracTickets for help on using tickets.