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:
-
FooCount :: EntityField Foo Int
- this is known. -
update :: Key rec -> [Update rec]
- this is known. -
FooCount =. 1
turns into a constraint(Num a, SqlAssignment lhs a result)
. - The
update
causesresult
to be known asUpdate Foo
, which is sufficient to select theSqlAssignment lhs rhs (Persistent.Update rec)
instance. - This introduces some wanted constraints:
lhs ~ EntityField rec' typ'
,rhs ~ typ'
, and finallyrec ~ rec'
. Crucially, we introduce these as type equality constraints. -
lhs ~ EntityField rec' typ'
is fine - we getEntityField Foo Int
, which propagates torhs ~ tyc ~ Int
andrec' ~ Foo ~ rec
, so we have inferredUpdate Foo
as ourresult
type. - Finally, to
update
- we have a type ofupdate :: (rec ~ Foo) => Key rec -> [Update rec]
. But our subexpression on theupdate
iscoerce barId
. -
coerce barId
has a typeCoercible (Key Bar) r => r
.Coercible
is a magically instantiated class, and something about how ther ~ 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