Support wild cards in data/type family instances
authorThomas Winant <thomas.winant@cs.kuleuven.be>
Mon, 3 Aug 2015 12:57:40 +0000 (14:57 +0200)
committerBen Gamari <ben@smart-cactus.org>
Mon, 3 Aug 2015 12:58:21 +0000 (14:58 +0200)
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

16 files changed:
compiler/rename/RnSource.hs
compiler/typecheck/TcTyClsDecls.hs
docs/users_guide/7.12.1-notes.xml
docs/users_guide/glasgow_exts.xml
testsuite/tests/partial-sigs/should_compile/DataFamilyInstanceLHS.hs [new file with mode: 0644]
testsuite/tests/partial-sigs/should_compile/DataFamilyInstanceLHS.stderr [new file with mode: 0644]
testsuite/tests/partial-sigs/should_compile/TypeFamilyInstanceLHS.hs [new file with mode: 0644]
testsuite/tests/partial-sigs/should_compile/TypeFamilyInstanceLHS.stderr [new file with mode: 0644]
testsuite/tests/partial-sigs/should_compile/all.T
testsuite/tests/partial-sigs/should_fail/NamedWildcardInDataFamilyInstanceLHS.hs [new file with mode: 0644]
testsuite/tests/partial-sigs/should_fail/NamedWildcardInDataFamilyInstanceLHS.stderr [new file with mode: 0644]
testsuite/tests/partial-sigs/should_fail/NamedWildcardInTypeFamilyInstanceLHS.hs [new file with mode: 0644]
testsuite/tests/partial-sigs/should_fail/NamedWildcardInTypeFamilyInstanceLHS.stderr [new file with mode: 0644]
testsuite/tests/partial-sigs/should_fail/WildcardInTypeFamilyInstanceLHS.hs [deleted file]
testsuite/tests/partial-sigs/should_fail/WildcardInTypeFamilyInstanceLHS.stderr [deleted file]
testsuite/tests/partial-sigs/should_fail/all.T

index 8396e84..f6a3007 100644 (file)
@@ -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
index 2c18d5e..3750be8 100644 (file)
@@ -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
index e00706c..b2cb369 100644 (file)
                <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>
 
index b6c01d6..f6a4403 100644 (file)
@@ -6099,6 +6099,24 @@ data instance GMap (Either a b) v = GMapEither (GMap a v) (GMap b v)
       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
       requires the class declaration to be visible.  Moreover, each instance
@@ -6251,6 +6269,13 @@ type instance Elem [e] = e
     </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
       require the class declaration to be visible. Moreover, each instance
@@ -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.
diff --git a/testsuite/tests/partial-sigs/should_compile/DataFamilyInstanceLHS.hs b/testsuite/tests/partial-sigs/should_compile/DataFamilyInstanceLHS.hs
new file mode 100644 (file)
index 0000000..68541b8
--- /dev/null
@@ -0,0 +1,13 @@
+{-# 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
diff --git a/testsuite/tests/partial-sigs/should_compile/DataFamilyInstanceLHS.stderr b/testsuite/tests/partial-sigs/should_compile/DataFamilyInstanceLHS.stderr
new file mode 100644 (file)
index 0000000..6ca37a9
--- /dev/null
@@ -0,0 +1,16 @@
+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]
diff --git a/testsuite/tests/partial-sigs/should_compile/TypeFamilyInstanceLHS.hs b/testsuite/tests/partial-sigs/should_compile/TypeFamilyInstanceLHS.hs
new file mode 100644 (file)
index 0000000..c3172b7
--- /dev/null
@@ -0,0 +1,9 @@
+{-# 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
diff --git a/testsuite/tests/partial-sigs/should_compile/TypeFamilyInstanceLHS.stderr b/testsuite/tests/partial-sigs/should_compile/TypeFamilyInstanceLHS.stderr
new file mode 100644 (file)
index 0000000..b2ead26
--- /dev/null
@@ -0,0 +1,13 @@
+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]
index 5597183..9e7b8a7 100644 (file)
@@ -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'])
diff --git a/testsuite/tests/partial-sigs/should_fail/NamedWildcardInDataFamilyInstanceLHS.hs b/testsuite/tests/partial-sigs/should_fail/NamedWildcardInDataFamilyInstanceLHS.hs
new file mode 100644 (file)
index 0000000..65bad72
--- /dev/null
@@ -0,0 +1,10 @@
+{-# 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
diff --git a/testsuite/tests/partial-sigs/should_fail/NamedWildcardInDataFamilyInstanceLHS.stderr b/testsuite/tests/partial-sigs/should_fail/NamedWildcardInDataFamilyInstanceLHS.stderr
new file mode 100644 (file)
index 0000000..f97cdc3
--- /dev/null
@@ -0,0 +1,4 @@
+
+NamedWildcardInDataFamilyInstanceLHS.hs:8:21: error:
+    Unexpected wild card: ‘_a’
+    In the data type declaration for ‘Sing’
diff --git a/testsuite/tests/partial-sigs/should_fail/NamedWildcardInTypeFamilyInstanceLHS.hs b/testsuite/tests/partial-sigs/should_fail/NamedWildcardInTypeFamilyInstanceLHS.hs
new file mode 100644 (file)
index 0000000..dabd781
--- /dev/null
@@ -0,0 +1,5 @@
+{-# LANGUAGE NamedWildCards #-}
+module NamedWildcardInTypeFamilyInstanceLHS where
+
+type family F a where
+  F _t = Int
diff --git a/testsuite/tests/partial-sigs/should_fail/NamedWildcardInTypeFamilyInstanceLHS.stderr b/testsuite/tests/partial-sigs/should_fail/NamedWildcardInTypeFamilyInstanceLHS.stderr
new file mode 100644 (file)
index 0000000..550f6ce
--- /dev/null
@@ -0,0 +1,4 @@
+
+NamedWildcardInTypeFamilyInstanceLHS.hs:5:5: error:
+    Unexpected wild card: ‘_t’
+    In the declaration for type synonym ‘F’
diff --git a/testsuite/tests/partial-sigs/should_fail/WildcardInTypeFamilyInstanceLHS.hs b/testsuite/tests/partial-sigs/should_fail/WildcardInTypeFamilyInstanceLHS.hs
deleted file mode 100644 (file)
index 3fca6bc..0000000
+++ /dev/null
@@ -1,8 +0,0 @@
-{-# LANGUAGE PartialTypeSignatures, TypeFamilies, InstanceSigs #-}
-module WildcardInTypeFamilyInstanceLHS where
-
-class Foo k where
-  type Dual k :: *
-
-instance Foo Int where
-  type Dual _ = Maybe Int
diff --git a/testsuite/tests/partial-sigs/should_fail/WildcardInTypeFamilyInstanceLHS.stderr b/testsuite/tests/partial-sigs/should_fail/WildcardInTypeFamilyInstanceLHS.stderr
deleted file mode 100644 (file)
index fda3e6b..0000000
+++ /dev/null
@@ -1,6 +0,0 @@
-
-WildcardInTypeFamilyInstanceLHS.hs:8:13:
-    Unexpected wild card: ‘_’
-    In the type ‘_’
-    In the type instance declaration for ‘Dual’
-    In the instance declaration for ‘Foo Int’
index 9417a3e..8f0b0a0 100644 (file)
@@ -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, [''])