#15431 closed bug (fixed)

Coercible and Existential types don't play nicely

Reported by: NioBium Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.4.3
Keywords: Roles Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #14333 Differential Rev(s):
Wiki Page:

Description

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

Change History (5)

comment:1 Changed 14 months ago by RyanGlScott

Keywords: Roles added

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 or not.

comment:2 Changed 14 months ago by goldfire

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.

comment:3 Changed 14 months ago by Simon Peyton Jones <simonpj@…>

In f0d27f5/ghc:

Stop marking soluble ~R# constraints as insoluble

We had a constraint (a b ~R# Int), and were marking it as 'insoluble'.
That's bad; it isn't.  And it caused Trac #15431. Soultion is simple.

I did a tiny refactor on can_eq_app, so that it is used only for
nominal equalities.

comment:4 Changed 14 months ago by simonpj

Status: newmerge

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 (comment:10) does the symmetry bit. I agree that incompleteness is still lurking!

The fix is a modest one; could be merged.

comment:5 Changed 14 months ago by bgamari

Resolution: fixed
Status: mergeclosed
Note: See TracTickets for help on using tickets.