coercion and identity with constraints in Haskell

user_242189 0
Viewed 77

Is there a reason why coerce does not have a default for the identity with respect to constraints ?


import Data.Coerce
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --

newtype Id a = Id a

a :: Id Int
a = coerce 3 -- bad

-- • Couldn't match representation of type ‘a0’ with that of ‘Int’ arising from a use of ‘coerce’
-- • Ambiguous type variable ‘a0’ arising from the literal ‘3’
--   prevents the constraint ‘(Num a0)’ from being solved.
--   Probable fix: use a type annotation to specify what ‘a0’ should be.
--   These potential instances exist:
--     instance Num Integer -- Defined in ‘GHC.Num’
--     instance Num Double -- Defined in ‘GHC.Float’
--     instance Num Float -- Defined in ‘GHC.Float’

b :: Id Int
b = coerce (3 :: Int)

I imagined that it could attempt to solve that with a0 ~ Int (or other constraints in general), as the identity (and merging contraints) seems always an option

haskell
2 Answers

The following code is inherently ambiguous

a :: Id Int
a = coerce 3

because it actually means

a :: Id Int
a = coerce (fromInteger (3 :: Integer))

and here fromInteger could return any type T in class Num, as long as T can be converted to Id Int by coerce.

One possible solution is, of course, T ~ Int, but it's not the only one. Consider this contrived example:

newtype T = T Int

instance Num T where
   fromInteger n = T (fromInteger n + 1)

a :: Id Int
a = coerce (3 :: T)
-- which means  a = coerce (fromInteger (3 :: Integer) :: T)

Here, we have a = Id 4 because fromInteger incremented the Int, which differs from the Id 3 we would get from a = coerce (3 :: Int).

When performing type inference on coerce 3, Haskell can not know if we mean coerce (3 :: Int) or coerce (3 :: T), so the code is inherently ambiguous, and rejected as such.

user_32349590

If I understand the question correctly, I think the answer is probably the boring one: nobody has had both the idea and the time to do the engineering work needed to add that special case to the type checker. I don't see a technical reason not to do it, and if you emitted a warning each time such defaulting was done (or hid it behind a language extension, or both) I think it's reasonably likely GHC HQ would accept such a patch.

user_7916040
Related