I have encountered a similar inconsistency:
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE QuantifiedConstraints #-}
module Test where
class VectorSpace v where
type Scalar v
(*^) :: Scalar v -> v -> v
class (VectorSpace v, Scalar v ~ a) => VectorSpaceOver a v
class (forall a n. FamScalar v ~ a => VectorSpaceOver a (v n)) => VectorSpaceFamily v where
type FamScalar v
works :: VectorSpaceFamily v => FamScalar v -> v n -> v n
works = (*^)
fails :: VectorSpaceFamily v => FamScalar v -> v n -> v n
fails a v = a *^ v
GHC typechecks works
, but it's unable to handle fails
:
Test.hs:20:13: error:
• Could not deduce: FamScalar v ~ Scalar (v n)
from the context: VectorSpaceFamily v
bound by the type signature for:
fails :: forall {k} (v :: k -> *) (n :: k).
VectorSpaceFamily v =>
FamScalar v -> v n -> v n
at Test.hs:19:1-57
• In the first argument of ‘(*^)’, namely ‘a’
In the expression: a *^ v
In an equation for ‘fails’: fails a v = a *^ v
• Relevant bindings include
v :: v n (bound at Test.hs:20:9)
a :: FamScalar v (bound at Test.hs:20:7)
fails :: FamScalar v -> v n -> v n (bound at Test.hs:20:1)
|
20 | fails a v = a *^ v
| ^
Which is surprising for me, because I see works
and fails
as pretty much identical.