GitLab

It would be nice to allow users to write Coercible instances in signature files, to indicate "this can be instantiated to any type that is Coercible to some other type". Random example:

{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE UnboxedTuples #-}

unit number-unknown where
  signature NumberUnknown where
    import Data.Coerce
    data Number
    instance Coercible Number Int
    op :: Number -> Number -> Number
  module NumberStuff where
    import Data.Coerce
    import NumberUnknown
    funcA :: Number -> Number -> Int
    funcA x y = coerce (op x y)

unit number-int where
  module NumberUnknown where
    type Number = Int
    op :: Int -> Int -> Int
    op = (+)

unit number-times where
  module NumberUnknown where
    newtype Number = MkNumber Int
    op :: Number -> Number -> Number
    op (MkNum x) (MkNum y) = MkNum (x * y)

unit main where
  dependency number-unknown[NumberUnknown=number-times:NumberUnknown]
  module Main where
    import NumberUnknown
    import NumberStuff
    import GHC.Types
    main = print (funcA (MkNumber 3) (MkNumber 5))

This is currently rejected with:

error:
    * Class `Coercible' does not support user-specified instances.
    * In the instance declaration for `Coercible Number Int'
   |
10 |     instance Coercible Number Int
   |              ^^^^^^^^^^^^^^^^^^^^

However, it's not as simple as disabling the check, as it seems that GHC's solver for ~#R is not smart enough to pick up the Coercible instance, as we then get:

error:
    * Couldn't match representation of type `Number' with that of `Int'
        arising from a use of `coerce'
      NB: The type constructor `Number' is abstract
    * In the expression: coerce (op x y)
      In an equation for `funcA': funcA x y = coerce (op x y)
   |
16 |     funcA x y = coerce (op x y)
   |                 ^^^^^^

I assume that this could be remedied by allowing top-level interactions for (~#), similar to what I have done for Concrete in !6164 (closed).