Opened 2 years ago

Closed 17 months ago

#14333 closed bug (fixed)

GHC doesn't use the fact that Coercible is symmetric

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.2.1
Keywords: TypeFamilies, Roles Cc: RyanGlScott
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_compile/T14333
Blocked By: Blocking:
Related Tickets: #14323, #15431 Differential Rev(s):
Wiki Page:

Description

{-# Language ScopedTypeVariables, GADTs, DeriveGeneric #-}

import GHC.Generics
import Data.Type.Coercion

data AB = A | B deriving (Generic)
data XY = X | Y deriving (Generic)

data This ab xy where
  At :: This AB XY

foo :: This ab xy -> Coercion (Rep ab a) (Rep xy a)
foo At = Coercion

bar :: forall ab xy a. This ab xy -> Coercion (Rep ab a) (Rep xy a)
bar at
  | Coercion <- foo at :: Coercion (Rep ab a) (Rep xy a)
  = Coercion

This compiles on 8.2.1 and 8.3.20170920 but flipping the arguments to Coercion fails

-- ...

-- • Could not deduce: Coercible (Rep xy a) (Rep ab a)
--     arising from a use of ‘Coercion’
--   from the context: Coercible (Rep ab a) (Rep xy a)
--     bound by a pattern with constructor:

bar :: forall ab xy a. This ab xy -> Coercion (Rep xy a) (Rep ab a)
bar at
  | Coercion <- foo at :: Coercion (Rep ab a) (Rep xy a)
  = Coercion

Conceptually there should be an (Undecidable) superclass constraint for Coercible

class Coercible b a => Coercible a b

Attachments (1)

SelfContained.hs (2.0 KB) - added by Iceland_jack 2 years ago.

Download all attachments as: .zip

Change History (16)

comment:1 Changed 2 years ago by RyanGlScott

Cc: RyanGlScott added
Keywords: TypeFamilies added

Indeed, something funny is going on here.

Here's a simplified version of this program. Notice that this typechecks:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Type.Coercion

type family F a b :: *

f :: Coercion (F a b) (F c d) -> Coercion (F c d) (F a b)
f Coercion = Coercion

However, if you change the kind of F:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Type.Coercion

type family F a :: * -> *

f :: Coercion (F a b) (F c d) -> Coercion (F c d) (F a b)
f Coercion = Coercion

Then it no longer typechecks:

GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/ryanglscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

Bug.hs:10:14: error:
    • Could not deduce: Coercible (F c d) (F a b)
        arising from a use of ‘Coercion’
      from the context: Coercible (F a b) (F c d)
        bound by a pattern with constructor:
                   Coercion :: forall k (a :: k) (b :: k).
                               Coercible a b =>
                               Coercion a b,
                 in an equation for ‘f’
        at Bug.hs:10:3-10
      NB: ‘F’ is a type function, and may not be injective
    • In the expression: Coercion
      In an equation for ‘f’: f Coercion = Coercion
    • Relevant bindings include
        f :: Coercion (F a b) (F c d) -> Coercion (F c d) (F a b)
          (bound at Bug.hs:10:1)
   |
10 | f Coercion = Coercion
   |              ^^^^^^^^

Of course, it's quite easy to actually construct an implementation of f which does typecheck:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Type.Coercion

type family F a :: * -> *

f :: Coercion (F a b) (F c d) -> Coercion (F c d) (F a b)
f = sym

So the mystery is why GHC gets tripped up on this particular incarnation of F.

comment:2 Changed 2 years ago by goldfire

This is a good point. The problem is that (a b) ~R# (c d) tells you nothing at all about the relationship between any of the variables a, b, c, and d. This isn't a restriction in the solver, but simply a truism of representational equality. So when GHC knows (a b) ~R# (c d), it is too stupid to figure out (c d) ~R# (a b). I can thus boil down the problem even further:

bad :: Coercible (a b) (c d) => c d -> a b
bad = coerce

will fail to type-check. (The version with argument & result swapped works fine.)

Could the solver work around this? Maybe, with sufficient cleverness. (Unlike my concerns around recursive newtypes, I think this may be an engineering issue, not undecidability.) I don't think it would be easy though, requiring some kind of flattening logic akin to what GHC does for type families.

Do you have a concrete use case?

comment:3 Changed 2 years ago by simonpj

Keywords: Roles added

comment:4 in reply to:  2 Changed 2 years ago by Iceland_jack

Replying to goldfire:

Do you have a concrete use case?

My use case is this where swap is required to express symmetry. I use this to witness a coercion between Rep a x and Rep b x

sameRep :: SameRep a b :- (Rep a x `Coercible` Rep b x)

but I also need

SameRep a b :- (Rep b x `Coercible` Rep a x)

for which I use swap

comment:5 Changed 2 years ago by goldfire

Could you include the full code of the concrete use case? I followed the link, but that's a non-trivial and not-self-contained file.

GHC accepts

f :: Coercible b a => a x -> b x
f = coerce

So, if SameRep a b implies Coercible (Rep a) (Rep b), then the final implication above should hold. If, on the other hand, SameRep a b implies forall x. Coercible (Rep a x) (Rep b x), then you're in trouble (at least with the current implementation).

It occurs to me that you do not necessarily need to do anything clever with a b ~R# c d, but instead F a b ~R# F c d, where F has an arity of 1. Tackling the special case where we have a type function at the head, instead of any variable, might be easier than the general case.

Changed 2 years ago by Iceland_jack

Attachment: SelfContained.hs added

comment:6 Changed 2 years ago by Iceland_jack

I attached an example, I found another need for this: encoding that the opposite category is coercible to the current (based on hask):

type Cat obj = obj -> obj -> Type

class (forall xx yy. Coercible (cat xx yy) (Op cat yy xx)) => Category (cat :: Cat obj) where
  type Op cat :: Cat obj

The use case is similar as the other one but I can elaborate if needed. In my current implementation I want to coerce between opposite categories but I needed to assume that both directions hold to get both op & unop

op :: forall cat a b. Category cat => cat a b -> Op cat b a                                                                                                                                                   
op = coerce                                                                                                                                                                                                         
  \\ coer @cat @a @b                                                                                                                                                                                                
                                                                                                                                                                                                                    
unop :: forall cat a b. Category cat => Op cat b a -> cat a b                                                                                                                                                 
unop = coerce                                                                                                                                                                                                       
  \\ coer @cat @a @b                                                                                                                                                                                                
Last edited 2 years ago by Iceland_jack (previous) (diff)

comment:7 Changed 2 years ago by simonpj

I found I could do this quite easily. (I happened to be in the area.) Patch coming.

comment:8 Changed 2 years ago by Iceland_jack

Good news!

comment:9 in reply to:  7 Changed 2 years ago by goldfire

Replying to simonpj:

I found I could do this quite easily. (I happened to be in the area.) Patch coming.

Ooh. I'm curious. I'm not yet ready to backtrack from my opinion that this would be hard.

comment:10 Changed 2 years ago by Simon Peyton Jones <simonpj@…>

In 5a66d57/ghc:

Better solving for representational equalities

This patch adds a bit of extra solving power for representational
equality constraints to fix Trac #14333

The main changes:

* Fix a buglet in TcType.isInsolubleOccursCheck which wrongly
  reported a definite occurs-check error for (a ~R# b a)

* Get rid of TcSMonad.emitInsolubles.  It had an ad-hoc duplicate-removal
  piece that is better handled in interactIrred, now that insolubles
  are Irreds.

  We need a little care to keep inert_count (which does not include
  insolubles) accurate.

* Refactor TcInteract.solveOneFromTheOther, to return a much simpler
  type.  It was just over-complicated before.

* Make TcInteract.interactIrred look for constraints that match
  either way around, in TcInteract.findMatchingIrreds

This wasn't hard and it cleaned up quite a bit of code.

comment:11 Changed 2 years ago by simonpj

Ooh. I'm curious.

OK, take a look. Most of the patch is good regardless. If you disagree with the payload of the change (matching either way round) it'd be one-line change to take it out again.

comment:12 Changed 2 years ago by RyanGlScott

Commit 5a66d574890ed09859ca912c9e0969dba72f4a23 fixed #14323 as well, so if the payload of that commit is reverted, make sure to re-open #14323 as well.

comment:13 Changed 2 years ago by goldfire

Your patch solves a smaller problem than I was thinking of... but now I can't seem to think of it again. Regardless, your patch looks correct to me.

comment:14 Changed 17 months ago by RyanGlScott

Is this bug fixed?

(Also, see #15431 for a possibly related issue.)

comment:15 Changed 17 months ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: typecheck/should_compile/T14333

Yes I believe this is fixed

Note: See TracTickets for help on using tickets.