Coercible and Existential types don't play nicely

In the following example, f compiles but g doesn't.

data T t where
  A :: Show (t a) => t a -> T t
  B :: Coercible Int (t a) => t a -> T t

f :: T t -> String
f (A t) = show t

g :: T t -> Int
g (B t) = coerce t

• Couldn't match representation of type ‘Int’ with that of ‘t a’
  Inaccessible code in
    a pattern with constructor:
      B :: forall k (t :: k -> *) (a :: k).
           Coercible Int (t a) =>
           t a -> T t,
    in an equation for ‘g’
• In the pattern: B t
  In an equation for ‘g’: g (B t) = coerce t

Trac metadata

Trac field	Value
Version	8.4.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

mentioned in issue #14333 (closed)

changed milestone to %8.6.1

changed weight to 5

added Tbug Trac import labels

Hm, this is interesting. This can be minimized to the following examples, which are slight variations of each other:

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
module Bug where

import Data.Coerce
import Data.Functor.Identity

g1 :: Coercible (t a) Int => t a -> Int
g1 = coerce

g2 :: Coercible Int (t a) => t a -> Int
g2 = coerce

g1 typechecks, but g2 doesn't!

$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:12:6: error:
    • Couldn't match representation of type ‘t a’ with that of ‘Int’
        arising from a use of ‘coerce’
    • In the expression: coerce
      In an equation for ‘g2’: g2 = coerce
    • Relevant bindings include g2 :: t a -> Int (bound at Bug.hs:12:1)
   |
12 | g2 = coerce
   |      ^^^^^^

I'm not sure if this is related to #14333 (closed) or not.

Trac metadata

Trac field	Value
Related	- → #14333 (closed)

added roles label

I'm not all that surprised here. GHC has no way of decomposing Coercible Int (t a), and so it just remembers that constraint in case it needs to prove exactly Coercible Int (t a). In this case, it's trying to prove Coercible (t a) Int, and so it gives up.

I suppose we special-case the lookup to include looking for a symmetrical constraint, but there will always be incompleteness lurking around the corner.

mentioned in commit f0d27f51

There was a palpable bug that meant the constraint was marked as insoluble, when it wasn't. This fixes both the OP and coment:1.

The fix in #14333 (closed) (comment:10) does the symmetry bit. I agree that incompleteness is still lurking!

The fix is a modest one; could be merged.

added 1 deleted label

closed

Merged with 09abd1c4.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

removed 1 deleted label

added Pnormal label