Coercible constraints should be picked arbitrarily

Summary

Coercible constraints should be picked arbitrarily, in the absence of other, computationally-relevant constraints.

Steps to reproduce

Consider the following program.

{-# LANGUAGE TypeApplications #-}

import Data.IntMap (IntMap, mapKeysMonotonic, Key)
import Data.Coerce (coerce)

newtype MyMap = MyMap (IntMap Bool)

doesn'tWork :: (Key -> Key) -> MyMap -> MyMap
doesn'tWork = coerce mapKeysMonotonic

works :: (Key -> Key) -> MyMap -> MyMap
works = coerce (mapKeysMonotonic @Bool)

mapKeysmonotonic has type

(Key -> Key) -> IntMap a -> IntMap a

and we attempt to coerce it to type

(Key -> Key) -> MyMap -> MyMap

since MyMap is a newtype around IntMap Bool this ends up generating the constraint

Coercible a Bool

and there is no way to specify that constraint given that a doesn't otherwise appear in the top-level type. Hence doesn'tWork will not type check. If I force the type of a to be Bool using a TypeApplication then it does type check (works).

But is this a missing feature of GHC's Coercible system? Since a is not otherwise constrained is it not valid for GHC to choose it to be Bool? Coercible instances contain no observable content so no observable behaviour could depend on the particular choice of Coercible a Bool instance, and choosing a ~ Bool is the natural one.

(Discussed earlier on haskell-cafe)

Expected behavior

GHC picks a ~ Bool.

Environment

GHC 8.10, 9.2

added needs triage label

assigned to @rae

It's more like seeing a residual constraint Num alpha and resolving alpha := Integer in type-class defaulting. Here we see Coercible alpha Bool and we want to resolve alpha := Bool.

So yes, not too hard. Do it in applyDefaultingRules, I think

You should also be able to do this with a defaulting plugin.

added Plow Tfeature request defaulting labels and removed needs triage label

I'm not sure whether we should change this behaviour in GHC itself; it seems like a rather major change, although I agree it can make working with coerce a lot easier, as sometimes it requires a bit too many type annotations to get GHC to understand what one wants to do.

It might be worth writing a simple defaulting plugin that does defaulting in unsolved Coercible constraints, and seeing if enabling it has any unexpected impacts.

it seems like a rather major change

I don't think it's really a major change. Its just the top-level defaulting in simplifyTop. I think it'd make perfect sense. I wonder what @rae thinks.

It's a bit like -XExtendedDefaultRules. I guess you could make it an extension flag.

unassigned @rae

mentioned in merge request !13834 (closed)

I have added the defaulting described in #21003 (comment 403942) in !13834 (closed). The program from the OP is accepted with that change.

Super, thanks!

Moreover there is a test for #21003 (closed) in !13834 (closed).

changed the description

mentioned in issue #25416

mentioned in issue #25825

mentioned in commit 2793eb47

closed with commit 1e53277a

mentioned in commit 1e53277a

Fixed by

commit 1e53277af36d3f0b6ad5491f70ffc5593a49dcfd
Author: sheaf <sam.derbyshire@gmail.com>
Date:   Tue Jan 21 11:22:57 2025 +0100

    Allow defaulting of representational equalities
    
    This commit generalises the defaulting of equality constraints that
    was introduced in 663daf8d (with follow-up in 6863503c) to allow
    the defaulting of *representational* equality constraints.
    
    Now we default a representational equality
    
      ty1 ~R# ty2
    
    by unifying ty1 ~# ty2.
    
    This allows the following defaulting to take place:
    
      - Coercible alpha[tau] Int ==> alpha := Int
      - Coercible (IO beta[tau]) (IO Char) ==> beta := Char
    
    See Note [Defaulting representational equalities] in GHC.Tc.Solver.Default
    for more details.
    
    Fixes #21003

 compiler/GHC/Tc/Solver/Default.hs                          | 149 ++++++++++++++++++++++++++++++++++++++------
 compiler/GHC/Tc/Solver/Dict.hs                             |   6 +-
 compiler/GHC/Tc/Solver/Equality.hs                         |   4 ++
 compiler/GHC/Tc/Solver/Monad.hs                            |   4 +-
 compiler/GHC/Tc/Utils/Unify.hs                             |   2 +-
 docs/users_guide/9.14.1-notes.rst                          |   4 ++
 testsuite/tests/default/default-fail08.hs                  |  14 +++--
 testsuite/tests/default/default-fail08.stderr              |  28 +++++++--
 testsuite/tests/rep-poly/T14561b.stderr                    |   4 +-
 testsuite/tests/rep-poly/UnliftedNewtypesCoerceFail.stderr |   4 +-
 testsuite/tests/typecheck/should_compile/T21003.hs         |  35 +++++++++++
 testsuite/tests/typecheck/should_compile/all.T             |   1 +
 testsuite/tests/typecheck/should_fail/T10495.hs            |   5 +-
 testsuite/tests/typecheck/should_fail/T10495.stderr        |  11 ++--
 14 files changed, 222 insertions(+), 49 deletions(-)