Type checking influenced by definition
Here's a program, taken from !8820 (comment 486855)
{-# LANGUAGE DataKinds, TypeFamilies, TypeFamilyDependencies #-}
module M where
import Data.Kind
import GHC.TypeLits
data Tuple2 x y = MkTuple2 x y
type TupleArgKind :: Nat -> Type
type family TupleArgKind n = r | r -> n where
TupleArgKind 2 = Tuple2 Type Type
type Tuple :: forall (n :: Nat). TupleArgKind n -> Type
type family Tuple ts = r | r -> ts where
Tuple (MkTuple2 a b) = Tuple2 a b
-- works
f :: Tuple (MkTuple2 a b) -> ()
f (MkTuple2 _ _) = ()
-- fails
g :: Tuple (MkTuple2 a b) -> ()
g x = ()
-- works
h :: Tuple @2 (MkTuple2 a b) -> ()
h x = ()
f
and g
have the same type signature - but only g
is rejected because of an error in the type. This violates the principle that a type signature should stand on its own and not be influenced by the definition (unless PartialTypeSignatures
is enabled).
When typechecking the signature for f
, the relevant part from -ddump-tc-trace
(with wanted
added) is
kindGeneralizeSome
type: forall (a :: x_aFQ[tau:2]) (b :: y_aFR[tau:2]).
(Tuple (MkTuple2 a b |> {co_aFS}) -> () |> (TYPE {co_aMe})_N)
dvs: DV {dv_kvs = {x_aFQ[tau:2], y_aFR[tau:2], n_aFP[tau:2]},
dv_tvs = {}, dv_cvs = {co_aMh}}
wanted: WC {wc_impl =
Implic {
TcLevel = 2
Skolems = (a_aDb[sk:2] :: k_aFL[tau:2])
(b_aDc[sk:2] :: k_aFM[tau:2])
Given-eqs = NoGivenEqs
Status = Unsolved
Given =
Wanted =
WC {wc_simple =
[W] hole{co_aMh} {0}:: TupleArgKind n_aFP[tau:2]
GHC.Prim.~# Tuple2
x_aFQ[tau:2] y_aFR[tau:2] (CEqCan)}
Binds = CoEvBindsVar<aMf>
the type signature for ‘f’ }}
filtered_dvs: DV {dv_kvs = {}, dv_tvs = {}, dv_cvs = {co_aMh}}
Given a :: x, b :: y
, the expression Tuple @n (MkTuple2 a b)
is legal when TupleArgKind n ~ Tuple2 x y
. If generalized, the full type would be
f :: forall (n :: Nat) (x :: Type) (y :: Type) (a :: x) (b :: y). TupleArgKind n ~ Tuple2 x y => Tuple (MkTuple2 a b) -> ()
but that would require coercion quantification. So we do not generalize over x, y, n
. Later, in the case of f
, they are inferred to be Type, Type, 2
while in the case of g
, there are no further constraints and we error. Looks like we should reject f
just like g
.