Opened 20 months ago

Last modified 20 months ago

#14694 new bug

Incompleteness in the Coercible constraint solver

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

Description

$ ghci -ignore-dot-ghci
GHCi, version 8.5.20180105: http://www.haskell.org/ghc/  :? for help
Prelude> newtype WF f a = WF (f a)
Prelude> import Data.Coerce
Prelude Data.Coerce> :set -XFlexibleContexts 
Prelude Data.Coerce> :t coerce :: Coercible (cat a b) (a -> f b) => cat a b -> (a -> WF f b)

<interactive>:1:1: error:
    • Couldn't match representation of type ‘cat1 a1 b1’
                               with that of ‘a1 -> WF f1 b1’
        arising from a use of ‘coerce’
    • In the expression:
          coerce ::
            Coercible (cat a b) (a -> f b) => cat a b -> (a -> WF f b)

I'm not sure if I've filed this before or if it's even a bug.

But we know that Coercible (a -> f b) (a -> WF f b) so why doesn't this work?

Change History (5)

comment:1 Changed 20 months ago by goldfire

Keywords: Roles added

This is yet another incompleteness in the solver. A given like cat a b ~R (a -> f b) cannot be decomposed, as the typing rules for roles forbids this. Currently, GHC remembers the given and uses it only if a wanted matches the given exactly. Thus, this ticket.

One approach would be to have some structure that remembers cat a b maps to a -> f b and then use this to look up types. Actually, this wouldn't even be all that hard: the left-hand sides would all be AppTys (as plain old tyvars already have their own mechanism: CTyEqCan), and I believe just handling a top-level AppTy would be enough to make this approach complete. (I don't believe we'd ever need to look for a nested AppTy -- say, as the argument to a tycon -- because we'll decompose larger types until the AppTy bubbles up to the top.) We could just build a TrieMap mapping types to types; put a new entry in the TrieMap on given AppTy equalities and look up in the TrieMap on wanteds. Perhaps there's more to it than this, but I don't really think so.

Iceland_jack, do you remember if there's a place where we collect representational incompletenesses? This is not the first.

comment:2 Changed 20 months ago by simonpj

Just to be clear about what Richard means when he says "incompleteness", it's this: there is a solution, we don't find it.

Specifically we have

[G] (cat a b) ~R (a -> f b)
[W]  cat a b  ~R (a -> WF f b)

Applying the [G] transitively with the [W] wanted, we'd get

[W] (a -> f b) ~R (a -> WF f b)

which we can certainly solve easily. It's annoying that GHC's solver can't spot this.

comment:3 Changed 20 months ago by Iceland_jack

I don't remember a place where we collect them, we can make one & I can go through my old tickets in search for examples.

Here is another one maybe:

{-# Language FlexibleContexts #-}

import Data.Coerce

class Exp repr where
  int :: Int -> repr Int

newtype Coerce f a = Coerce (f a)

-- /tmp/Test.hs:13:9: error:
--     • Couldn't match representation of type ‘f Int’ with that of ‘Int’
--         arising from a use of ‘coerce’
--     • In the expression: coerce
--       In an equation for ‘int’: int = coerce
--       In the instance declaration for ‘Exp (Coerce f)’
--     • Relevant bindings include
--         int :: Int -> Coerce f Int (bound at /tmp/Test.hs:13:3)
--    |
-- 13 |   int = coerce
--    |         ^^^^^^
instance Coercible Int (f Int) => Exp (Coerce f) where
  int = coerce

but it works with int = Coerce . coerce.

comment:4 Changed 20 months ago by simonpj

Summary: Can't coerce given assumptionsIncompleteness in the Coercible constraint solver

comment:5 Changed 20 months ago by goldfire

The list of tickets on https://ghc.haskell.org/trac/ghc/wiki/Roles is short enough that I don't think it's necessary to specifically catalog the incompletnesses. When/if someone comes along ready to fix all this, we can put it together.

Note: See TracTickets for help on using tickets.