Allow user-written Coercible instances in signature files
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).