Commit d9d2102e authored by thomasw's avatar thomasw Committed by Ben Gamari
Browse files

Support wild cards in data/type family instances

Handle anonymous wild cards in type or data family instance
declarations like
unnamed type variables. For instance (pun intented):

    type family F (a :: *) (b :: *) :: *
    type instance F Int _ = Int

Is now the same as:

    type family F (a :: *) (b :: *) :: *
    type instance F Int x = Int

Note that unlike wild cards in partial type signatures, no errors (or
warnings
with -XPartialTypeSignatures) are generated for these wild cards, as
there is
nothing interesting to report to the user, i.e. the inferred kind.

Only anonymous wild cards are supported here, named and
extra-constraints wild
card are not.

Test Plan: pass new tests

Reviewers: goldfire, austin, simonpj, bgamari

Reviewed By: simonpj, bgamari

Subscribers: goldfire, thomie

Differential Revision: https://phabricator.haskell.org/D1092

GHC Trac Issues: #3699, #10586
parent 697079f1
......@@ -550,12 +550,19 @@ rnFamInstDecl doc mb_cls tycon pats payload rnPayload
; let all_fvs = fvs `addOneFV` unLoc tycon'
awcs = concatMap collectAnonymousWildCardNames pats'
; return (tycon',
HsWB { hswb_cts = pats', hswb_kvs = kv_names,
hswb_tvs = tv_names, hswb_wcs = [] },
hswb_tvs = tv_names, hswb_wcs = awcs },
payload',
all_fvs) }
-- type instance => use, hence addOneFV
where
collectAnonymousWildCardNames ty
= [ wildCardName wc
| L _ wc <- snd (collectWildCards ty)
, isAnonWildCard wc ]
rnTyFamInstDecl :: Maybe (Name, [Name])
-> TyFamInstDecl RdrName
......
......@@ -1009,7 +1009,8 @@ tc_fam_ty_pats :: FamTyConShape
-- (and, if C is poly-kinded, so will its kind parameter).
tc_fam_ty_pats (name, arity, kind)
(HsWB { hswb_cts = arg_pats, hswb_kvs = kvars, hswb_tvs = tvars })
(HsWB { hswb_cts = arg_pats, hswb_kvs = kvars
, hswb_tvs = tvars, hswb_wcs = wcs })
kind_checker
= do { let (fam_kvs, fam_body) = splitForAllTys kind
......@@ -1029,8 +1030,11 @@ tc_fam_ty_pats (name, arity, kind)
; let (arg_kinds, res_kind)
= splitKindFunTysN (length arg_pats) $
substKiWith fam_kvs fam_arg_kinds fam_body
-- Treat (anonymous) wild cards as type variables without a name.
-- See Note [Wild cards in family instances]
anon_tvs = [L (nameSrcSpan wc) (UserTyVar wc) | wc <- wcs]
hs_tvs = HsQTvs { hsq_kvs = kvars
, hsq_tvs = userHsTyVarBndrs loc tvars }
, hsq_tvs = anon_tvs ++ userHsTyVarBndrs loc tvars }
-- Kind-check and quantify
-- See Note [Quantifying over family patterns]
......@@ -1114,6 +1118,33 @@ none. The role of the kind signature (a :: Maybe k) is to add a constraint
that 'a' must have that kind, and to bring 'k' into scope.
Note [Wild cards in family instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Wild cards can be used in type/data family instance declarations to indicate
that the name of a type variable doesn't matter. Each wild card will be
replaced with a new unique type variable. For instance:
type family F a b :: *
type instance F Int _ = Int
is the same as
type family F a b :: *
type instance F Int b = Int
This is implemented as follows: during renaming anonymous wild cards are given
freshly generated names. These names are collected after renaming
(rnFamInstDecl) and used to make new type variables during type checking
(tc_fam_ty_pats). One should not confuse these wild cards with the ones from
partial type signatures. The latter generate fresh meta-variables whereas the
former generate fresh skolems.
Named and extra-constraints wild cards are not supported in type/data family
instance declarations.
Relevant tickets: #3699 and #10586.
************************************************************************
* *
Data types
......
......@@ -81,6 +81,15 @@
<literal>phantom</literal>, like it is in regular Haskell code.
</para>
</listitem>
<listitem>
<para>
Wildcards can be used in the type arguments of type/data
family instance declarations to indicate that the name of a
type variable doesn't matter. They will be replaced with new
unique type variables. See <xref
linkend="data-instance-declarations"/> for more details.
</para>
</listitem>
</itemizedlist>
</sect3>
......
......@@ -6098,6 +6098,24 @@ data instance GMap (Either a b) v = GMapEither (GMap a v) (GMap b v)
In this example, the declaration has only one variant. In general, it
can be any number.
</para>
<para>
When the name of a type argument of a data or newtype instance
declaration doesn't matter, it can be replaced with an underscore
(<literal>_</literal>). This is the same as writing a type variable with
a unique name.
<programlisting>
data family F a b :: *
data instance F Int _ = Int
-- Equivalent to
data instance F Int b = Int
</programlisting>
This resembles the wildcards that can be used in <xref
linkend="partial-type-signatures"/>. However, there are some
differences. Only anonymous wildcards are allowed in these instance
declarations, named and extra-constraints wildcards are not. No error
messages reporting the inferred types are generated, nor does the flag
<option>-XPartialTypeSignatures</option> have any effect.
</para>
<para>
Data and newtype instance declarations are only permitted when an
appropriate family declaration is in scope - just as a class instance declaration
......@@ -6250,6 +6268,13 @@ type instance Elem [e] = e
</programlisting>
</para>
<para>
Type arguments can be replaced with underscores (<literal>_</literal>)
if the names of the arguments don't matter. This is the same as writing
type variables with unique names. The same rules apply as for <xref
linkend="data-instance-declarations"/>.
</para>
<para>
Type family instance declarations are only legitimate when an
appropriate family declaration is in scope - just like class instances
......@@ -9413,6 +9438,12 @@ foo (x :: _) = (x :: _)
-- Inferred: forall w_. w_ -> w_
</programlisting>
<para>
Anonymous wildcards <emphasis>can</emphasis> occur in type or data instance
declarations. However, these declarations are not partial type signatures
and different rules apply. See <xref linkend="data-instance-declarations"/>
for more details.
</para>
<para>
Partial type signatures can also be used in <xref linkend="template-haskell"/> splices.
......
{-# LANGUAGE TypeFamilies, GADTs, DataKinds, PolyKinds #-}
module DataFamilyInstanceLHS where
-- Test case from #10586
data MyKind = A | B
data family Sing (a :: k)
data instance Sing (_ :: MyKind) where
SingA :: Sing A
SingB :: Sing B
foo :: Sing A
foo = SingA
TYPE SIGNATURES
foo :: Sing 'A
TYPE CONSTRUCTORS
data MyKind = A | B
Promotable
type role Sing nominal
data family Sing (a :: k)
RecFlag: Recursive
COERCION AXIOMS
axiom DataFamilyInstanceLHS.TFCo:R:SingMyKind_ ::
Sing = DataFamilyInstanceLHS.R:SingMyKind_
FAMILY INSTANCES
data instance Sing
Dependent modules: []
Dependent packages: [base-4.8.2.0, ghc-prim-0.4.0.0,
integer-gmp-1.0.0.0]
{-# LANGUAGE TypeFamilies #-}
module TypeFamilyInstanceLHS where
type family F (a :: *) (b :: *) :: *
type instance F Int _ = Int
type instance F Bool _ = Bool
foo :: F Int Char -> Int
foo = id
TYPE SIGNATURES
foo :: F Int Char -> Int
TYPE CONSTRUCTORS
type family F a b :: * open
COERCION AXIOMS
axiom TypeFamilyInstanceLHS.TFCo:R:FBool_ :: F Bool _ = Bool
axiom TypeFamilyInstanceLHS.TFCo:R:FInt_ :: F Int _ = Int
FAMILY INSTANCES
type instance F Int _
type instance F Bool _
Dependent modules: []
Dependent packages: [base-4.8.2.0, ghc-prim-0.4.0.0,
integer-gmp-1.0.0.0]
......@@ -6,6 +6,7 @@ test('AddAndOr4', normal, compile, ['-ddump-types -fno-warn-partial-type-signatu
test('AddAndOr5', normal, compile, ['-ddump-types -fno-warn-partial-type-signatures'])
test('AddAndOr6', normal, compile, ['-ddump-types -fno-warn-partial-type-signatures'])
test('BoolToBool', normal, compile, ['-ddump-types -fno-warn-partial-type-signatures'])
test('DataFamilyInstanceLHS', normal, compile, ['-ddump-types -fno-warn-partial-type-signatures'])
test('Defaulting1MROn', normal, compile, ['-ddump-types -fno-warn-partial-type-signatures'])
test('Defaulting2MROff', normal, compile, ['-ddump-types -fno-warn-partial-type-signatures'])
test('Defaulting2MROn', normal, compile, ['-ddump-types -fno-warn-partial-type-signatures'])
......@@ -43,6 +44,7 @@ test('ShowNamed', normal, compile, ['-ddump-types -fno-warn-partial-type-signatu
test('SimpleGen', normal, compile, ['-ddump-types -fno-warn-partial-type-signatures'])
test('SkipMany', normal, compile, ['-ddump-types -fno-warn-partial-type-signatures'])
test('SomethingShowable', normal, compile, ['-ddump-types -fno-warn-partial-type-signatures'])
test('TypeFamilyInstanceLHS', normal, compile, ['-ddump-types -fno-warn-partial-type-signatures'])
test('Uncurry', normal, compile, ['-ddump-types -fno-warn-partial-type-signatures'])
test('UncurryNamed', normal, compile, ['-ddump-types -fno-warn-partial-type-signatures'])
test('WarningWildcardInstantiations', normal, compile, ['-ddump-types'])
......
{-# LANGUAGE TypeFamilies, GADTs, DataKinds, PolyKinds, NamedWildCards #-}
module NamedWildcardInDataFamilyInstanceLHS where
data MyKind = A | B
data family Sing (a :: k)
data instance Sing (_a :: MyKind) where
SingA :: Sing A
SingB :: Sing B
NamedWildcardInDataFamilyInstanceLHS.hs:8:21: error:
Unexpected wild card: ‘_a’
In the data type declaration for ‘Sing’
{-# LANGUAGE NamedWildCards #-}
module NamedWildcardInTypeFamilyInstanceLHS where
type family F a where
F _t = Int
NamedWildcardInTypeFamilyInstanceLHS.hs:5:5: error:
Unexpected wild card: ‘_t’
In the declaration for type synonym ‘F’
{-# LANGUAGE PartialTypeSignatures, TypeFamilies, InstanceSigs #-}
module WildcardInTypeFamilyInstanceLHS where
class Foo k where
type Dual k :: *
instance Foo Int where
type Dual _ = Maybe Int
WildcardInTypeFamilyInstanceLHS.hs:8:13:
Unexpected wild card: ‘_’
In the type ‘_’
In the type instance declaration for ‘Dual’
In the instance declaration for ‘Foo Int’
......@@ -20,6 +20,8 @@ test('InstantiatedNamedWildcardsInConstraints', normal, compile_fail, [''])
test('NamedExtraConstraintsWildcard', normal, compile_fail, [''])
test('NamedWildcardInTypeSplice', normal, compile_fail, [''])
test('NamedWildcardsEnabled', normal, compile_fail, [''])
test('NamedWildcardInDataFamilyInstanceLHS', normal, compile_fail, [''])
test('NamedWildcardInTypeFamilyInstanceLHS', normal, compile_fail, [''])
test('NamedWildcardsNotEnabled', normal, compile_fail, [''])
test('NamedWildcardsNotInMonotype', normal, compile_fail, [''])
test('NestedExtraConstraintsWildcard', normal, compile_fail, [''])
......@@ -53,7 +55,6 @@ test('WildcardInPatSynSig', normal, compile_fail, [''])
test('WildcardInNewtype', normal, compile_fail, [''])
test('WildcardInStandaloneDeriving', normal, compile_fail, [''])
test('WildcardInstantiations', normal, compile_fail, [''])
test('WildcardInTypeFamilyInstanceLHS', normal, compile_fail, [''])
test('WildcardInTypeFamilyInstanceRHS', normal, compile_fail, [''])
test('WildcardInTypeSynonymLHS', normal, compile_fail, [''])
test('WildcardInTypeSynonymRHS', normal, compile_fail, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment