Skip to content

Potential bug/oddity in resolving `Coercible` constraints

Summary

The work codebase uses persistent and esqueleto, and esqueleto defines a bunch of operators that overlap/conflict with the persistent ones. This has become enough of an issue that I'm working on creating an abstraction for them.

(Persistent.=.) :: (PersistField typ) => EntityField rec typ -> typ -> Update rec

class SqlAssignment lhs rhs result where
  (=.) :: lhs -> rhs -> result

instance 
  ( PersistField typ, field ~ EntityField rec' typ', rec ~ rec', typ ~ typ'
  ) => SqlAssignment field typ (Persistent.Update rec) where
  (=.) = (Persistent.=.)

While working on this, I ran into an issue where Coercible constraints aren't being inferred correctly for instances of a data family. We have several lines like:

let fooId = coerce otherId
update fooId [FooName =. "hello"]

These lines compile fine with the =. from persistent, but fail with a "Couldn't match representation of type 'UUID' with that of 'Key Foo'` error.

update is a class member, given type:

class PersistStoreWrite backend where
  update :: forall record m. (MonadIO m, PersistRecordBackend record backend)
         => Key record -> [Update record] -> ReaderT backend m ()

So, here's my best guess:

GHC sees update (coerce barId) [FooCount =. 1], which causes it to start Inferring things:

  1. FooCount :: EntityField Foo Int - this is known.
  2. update :: Key rec -> [Update rec] - this is known.
  3. FooCount =. 1 turns into a constraint (Num a, SqlAssignment lhs a result).
  4. The update causes result to be known as Update Foo, which is sufficient to select the SqlAssignment lhs rhs (Persistent.Update rec) instance.
  5. This introduces some wanted constraints: lhs ~ EntityField rec' typ', rhs ~ typ', and finally rec ~ rec'. Crucially, we introduce these as type equality constraints.
  6. lhs ~ EntityField rec' typ' is fine - we get EntityField Foo Int, which propagates to rhs ~ tyc ~ Int and rec' ~ Foo ~ rec, so we have inferred Update Foo as our result type.
  7. Finally, to update - we have a type of update :: (rec ~ Foo) => Key rec -> [Update rec]. But our subexpression on the update is coerce barId.
  8. coerce barId has a type Coercible (Key Bar) r => r. Coercible is a magically instantiated class, and something about how the r ~ Foo is provided as an instance constraint defeats how the class can be solved out.

Steps to reproduce

Hey, fortunately a minimal reproducer fits in a single file!

{-# language TypeFamilies, TypeApplications, GADTs, FunctionalDependencies, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses #-}

module Lib where

import Data.Coerce
import Data.Proxy

update :: Key a -> [Proxy a] -> IO ()
update _ _ = pure ()

data User

data family Key a

newtype instance Key User = UserKey String

(=.) :: p a -> b -> Proxy a
(=.) _ _ = Proxy

class SqlAssignment lhs result where
    assignment :: proxy lhs -> rhs -> Proxy result

instance (rec ~ rec') => SqlAssignment rec rec' where
    assignment = (=.)

-- wtf
assignmentNoClass :: (rec ~ rec') => proxy rec -> b -> Proxy rec'
assignmentNoClass = assignment

userName :: Proxy User
userName = Proxy

someFunc :: IO ()
someFunc = do
    -- works: no class on `=.`
    update (coerce "hello") [userName =. "asdf"]
    -- works: type annotation on `coerce`
    update (coerce "asdf" :: Key User) [userName `assignment` "asdf"]
    --  works: somehow adding a top-level non-class-member makes this ok???
    update (coerce "asdf") [userName `assignmentNoClass` "asdf"]
    -- works: type signature on result of `assignment`
    update (coerce "asdf") [userName `assignment` "asdf" :: Proxy User]
    -- does not work
    update (coerce "asdf") [userName `assignment` "asdf"]

The data family appears to be relevant, here - given a newtype Key a = Key String, GHC is always able to deduce the Coercible (Key a) String. So I think the issue must be related to the data family in particular - just knowing (a ~ User) isn't enough to "unlock" that Coercible (Key User) String is valid, since that's a newtype. But literally any other type hint brings that information into scope.

Expected behavior

I expect that GHC can solve a Coercible a b constraint when b is known, even if that knowledge comes about through type equality constraints from instance resolution.

Environment

  • GHC version used: 8.10.7, 9.0.2, 9.2.7, 9.4.5, 9.6.1

Optional:

  • Operating System: Ubuntu
  • System Architecture: x86
Edited by parsonsmatt
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information