Fix the handling of instance signatures (Trac #9582, #9833)
authorSimon Peyton Jones <simonpj@microsoft.com>
Mon, 1 Dec 2014 11:43:20 +0000 (11:43 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Mon, 1 Dec 2014 11:48:15 +0000 (11:48 +0000)
This finally solves the issue of instance-method signatures that are
more polymorphic than the instanted class method.

See Note [Instance method signatures] in TcInstDcls.

A very nice fix for the two Trac tickets above.

12 files changed:
compiler/typecheck/TcBinds.lhs
compiler/typecheck/TcClassDcl.lhs
compiler/typecheck/TcInstDcls.lhs
docs/users_guide/glasgow_exts.xml
testsuite/tests/indexed-types/should_compile/T9582.hs [new file with mode: 0644]
testsuite/tests/indexed-types/should_compile/all.T
testsuite/tests/polykinds/T9833.hs [new file with mode: 0644]
testsuite/tests/polykinds/all.T
testsuite/tests/typecheck/should_fail/T6001.stderr
testsuite/tests/typecheck/should_fail/T7545.hs
testsuite/tests/typecheck/should_fail/T7545.stderr [deleted file]
testsuite/tests/typecheck/should_fail/all.T

index 6cd4203..f2f4b1a 100644 (file)
@@ -899,7 +899,6 @@ tcSpec poly_id prag@(SpecSig fun_name hs_tys inl)
                  (ptext (sLit "SPECIALISE pragma for non-overloaded function")
                   <+> quotes (ppr fun_name))
                   -- Note [SPECIALISE pragmas]
-        -- ; wraps <- mapM (tcSubType origin sig_ctxt (idType poly_id)) spec_tys
         ; wraps <- mapM (tcSubType sig_ctxt (idType poly_id)) spec_tys
         ; return [ (SpecPrag poly_id wrap inl) | wrap <- wraps ] }
   where
@@ -1371,8 +1370,8 @@ tcTySigs hs_sigs
        ; return (poly_ids, lookupNameEnv env, concat tyvarsl) }
 
 tcTySig :: LSig Name -> TcM ([TcSigInfo], [TcTyVar])
-tcTySig (L loc (IdSig id))
-  = do { sig <- instTcTySigFromId loc id
+tcTySig (L _ (IdSig id))
+  = do { sig <- instTcTySigFromId _ id
        ; return ([sig], []) }
 tcTySig (L loc (TypeSig names@(L _ name1 : _) hs_ty wcs))
   = setSrcSpan loc $
@@ -1411,9 +1410,10 @@ tcTySig (L loc (PatSynSig (L _ name) (_, qtvs) prov req ty))
        ; return ([TcPatSynInfo tpsi], []) }}
 tcTySig _ = return ([], [])
 
-instTcTySigFromId :: SrcSpan -> Id -> TcM TcSigInfo
-instTcTySigFromId loc id
-  = do { (tvs, theta, tau) <- tcInstType (tcInstSigTyVarsLoc loc)
+instTcTySigFromId :: Id -> TcM TcSigInfo
+instTcTySigFromId id
+  = do { let loc = getSrcSpan id
+       ; (tvs, theta, tau) <- tcInstType (tcInstSigTyVarsLoc loc)
                                          (idType id)
        ; return (TcSigInfo { sig_id = id, sig_loc = loc
                            , sig_tvs = [(Nothing, tv) | tv <- tvs]
@@ -1421,10 +1421,6 @@ instTcTySigFromId loc id
                            , sig_theta = theta, sig_tau = tau
                            , sig_extra_cts = Nothing
                            , sig_partial = False }) }
-    -- Hack: in an instance decl we use the selector id as
-    -- the template; but we do *not* want the SrcSpan on the Name of
-    -- those type variables to refer to the class decl, rather to
-    -- the instance decl
 
 instTcTySig :: LHsType Name -> TcType    -- HsType and corresponding TcType
             -> Maybe SrcSpan             -- Just loc <=> an extra-constraints
@@ -1432,7 +1428,7 @@ instTcTySig :: LHsType Name -> TcType    -- HsType and corresponding TcType
             -> [(Name, TcTyVar)] -> Name -> TcM TcSigInfo
 instTcTySig hs_ty@(L loc _) sigma_ty extra_cts nwcs name
   = do { (inst_tvs, theta, tau) <- tcInstType tcInstSigTyVars sigma_ty
-       ; return (TcSigInfo { sig_id = mkLocalId name sigma_ty
+       ; return (TcSigInfo { sig_id  = mkLocalId name sigma_ty
                            , sig_loc = loc
                            , sig_tvs = findScopedTyVars hs_ty sigma_ty inst_tvs
                            , sig_nwcs = nwcs
index 34409b2..769167f 100644 (file)
@@ -20,7 +20,7 @@ module TcClassDcl ( tcClassSigs, tcClassDecl2,
 import HsSyn
 import TcEnv
 import TcPat( addInlinePrags )
-import TcEvidence( idHsWrapper )
+import TcEvidence( HsWrapper, idHsWrapper )
 import TcBinds
 import TcUnify
 import TcHsType
@@ -225,7 +225,7 @@ tcDefMeth clas tyvars this_dict binds_in hs_sig_fn prag_fn (sel_id, dm_info)
                      <+> quotes (ppr sel_name))
 
            ; tc_bind <- tcInstanceMethodBody (ClsSkol clas) tyvars [this_dict]
-                                             dm_id_w_inline local_dm_sig
+                                             dm_id_w_inline local_dm_sig idHsWrapper
                                              IsDefaultMethod dm_bind
 
            ; return (unitBag tc_bind) }
@@ -233,10 +233,11 @@ tcDefMeth clas tyvars this_dict binds_in hs_sig_fn prag_fn (sel_id, dm_info)
 ---------------
 tcInstanceMethodBody :: SkolemInfo -> [TcTyVar] -> [EvVar]
                      -> Id -> TcSigInfo
+                     -> HsWrapper  -- See Note [Instance method signatures] in TcInstDcls
                      -> TcSpecPrags -> LHsBind Name
                      -> TcM (LHsBind Id)
 tcInstanceMethodBody skol_info tyvars dfun_ev_vars
-                     meth_id local_meth_sig
+                     meth_id local_meth_sig wrapper
                      specs (L loc bind)
   = do  { let local_meth_id = case local_meth_sig of
                   TcSigInfo{ sig_id = meth_id } -> meth_id
@@ -248,12 +249,13 @@ tcInstanceMethodBody skol_info tyvars dfun_ev_vars
                <- checkConstraints skol_info tyvars dfun_ev_vars $
                   tcPolyCheck NonRecursive no_prag_fn local_meth_sig lm_bind
 
-        ; let export = ABE { abe_wrap = idHsWrapper, abe_poly = meth_id
+        ; let export = ABE { abe_wrap = wrapper, abe_poly = meth_id
                            , abe_mono = local_meth_id, abe_prags = specs }
-              full_bind = AbsBinds { abs_tvs = tyvars, abs_ev_vars = dfun_ev_vars
-                                   , abs_exports = [export]
+              full_bind = AbsBinds { abs_tvs      = tyvars
+                                   , abs_ev_vars  = dfun_ev_vars
+                                   , abs_exports  = [export]
                                    , abs_ev_binds = ev_binds
-                                   , abs_binds = tc_bind }
+                                   , abs_binds    = tc_bind }
 
         ; return (L loc full_bind) }
   where
index acb5ae2..553af73 100644 (file)
@@ -917,60 +917,53 @@ tcSuperClasses dfun_id inst_tyvars dfun_ev_vars sc_theta
 
 ----------------------
 mkMethIds :: HsSigFun -> Class -> [TcTyVar] -> [EvVar]
-          -> [TcType] -> Id -> TcM (TcId, TcSigInfo)
+          -> [TcType] -> Id -> TcM (TcId, TcSigInfo, HsWrapper)
 mkMethIds sig_fn clas tyvars dfun_ev_vars inst_tys sel_id
-  = do  { let sel_occ = nameOccName sel_name
-        ; meth_name <- newName (mkClassOpAuxOcc sel_occ)
+  = do  { poly_meth_name  <- newName (mkClassOpAuxOcc sel_occ)
         ; local_meth_name <- newName sel_occ
                   -- Base the local_meth_name on the selector name, because
                   -- type errors from tcInstanceMethodBody come from here
-
-        ; local_meth_sig <- case lookupHsSig sig_fn sel_name of
-            Just hs_ty  -- There is a signature in the instance declaration
-               -> do { sig_ty <- check_inst_sig hs_ty
-                     ; instTcTySig hs_ty sig_ty Nothing [] local_meth_name }
+        ; let poly_meth_id  = mkLocalId poly_meth_name  poly_meth_ty
+              local_meth_id = mkLocalId local_meth_name local_meth_ty
+
+        ; case lookupHsSig sig_fn sel_name of
+            Just lhs_ty  -- There is a signature in the instance declaration
+                         -- See Note [Instance method signatures]
+               -> setSrcSpan (getLoc lhs_ty) $
+                  do { inst_sigs <- xoptM Opt_InstanceSigs
+                     ; checkTc inst_sigs (misplacedInstSig sel_name lhs_ty)
+                     ; sig_ty  <- tcHsSigType (FunSigCtxt sel_name) lhs_ty
+                     ; let poly_sig_ty = mkSigmaTy tyvars theta sig_ty
+                     ; tc_sig  <- instTcTySig lhs_ty sig_ty Nothing [] local_meth_name
+                     ; hs_wrap <- addErrCtxtM (methSigCtxt sel_name poly_sig_ty poly_meth_ty) $
+                                  tcSubType (FunSigCtxt sel_name) poly_sig_ty poly_meth_ty
+                     ; return (poly_meth_id, tc_sig, hs_wrap) }
 
             Nothing     -- No type signature
-               -> do { loc <- getSrcSpanM
-                     ; instTcTySigFromId loc (mkLocalId local_meth_name local_meth_ty) }
+               -> do { tc_sig <- instTcTySigFromId local_meth_id
+                     ; return (poly_meth_id, tc_sig, idHsWrapper) } }
               -- Absent a type sig, there are no new scoped type variables here
               -- Only the ones from the instance decl itself, which are already
               -- in scope.  Example:
               --      class C a where { op :: forall b. Eq b => ... }
               --      instance C [c] where { op = <rhs> }
               -- In <rhs>, 'c' is scope but 'b' is not!
-
-        ; let meth_id = mkLocalId meth_name meth_ty
-        ; return (meth_id, local_meth_sig) }
   where
     sel_name      = idName sel_id
+    sel_occ       = nameOccName sel_name
     local_meth_ty = instantiateMethod clas sel_id inst_tys
-    meth_ty       = mkForAllTys tyvars $ mkPiTypes dfun_ev_vars local_meth_ty
-
-    -- Check that any type signatures have exactly the right type
-    check_inst_sig hs_ty@(L loc _)
-       = setSrcSpan loc $
-         do { sig_ty <- tcHsSigType (FunSigCtxt sel_name) hs_ty
-            ; inst_sigs <- xoptM Opt_InstanceSigs
-            ; if inst_sigs then
-                unless (sig_ty `eqType` local_meth_ty)
-                       (badInstSigErr sel_name local_meth_ty)
-              else
-                addErrTc (misplacedInstSig sel_name hs_ty)
-            ; return sig_ty }
-
-badInstSigErr :: Name -> Type -> TcM ()
-badInstSigErr meth ty
-  = do { env0 <- tcInitTidyEnv
-       ; let tidy_ty = tidyType env0 ty
-                 -- Tidy the type using the ambient TidyEnv,
-                 -- to avoid apparent name capture (Trac #7475)
-                 --    class C a where { op :: a -> b }
-                 --    instance C (a->b) where
-                 --       op :: forall x. x
-                 --       op = ...blah...
-       ; addErrTc (hang (ptext (sLit "Method signature does not match class; it should be"))
-                      2 (pprPrefixName meth <+> dcolon <+> ppr tidy_ty)) }
+    poly_meth_ty  = mkSigmaTy tyvars theta local_meth_ty
+    theta         = map idType dfun_ev_vars
+
+methSigCtxt :: Name -> TcType -> TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc)
+methSigCtxt sel_name sig_ty meth_ty env0
+  = do { (env1, sig_ty)  <- zonkTidyTcType env0 sig_ty
+       ; (env2, meth_ty) <- zonkTidyTcType env1 meth_ty
+       ; let msg = hang (ptext (sLit "When checking that instance signature for") <+> quotes (ppr sel_name))
+                      2 (vcat [ ptext (sLit "is more general than its signature in the class")
+                              , ptext (sLit "Instance sig:") <+> ppr sig_ty
+                              , ptext (sLit "   Class sig:") <+> ppr meth_ty ])
+       ; return (env2, msg) }
 
 misplacedInstSig :: Name -> LHsType Name -> SDoc
 misplacedInstSig name hs_ty
@@ -989,6 +982,35 @@ tcSpecInstPrags dfun_id (InstBindings { ib_binds = binds, ib_pragmas = uprags })
        ; return (spec_inst_prags, mkPragFun uprags binds) }
 \end{code}
 
+Note [Instance method signatures]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+With -XInstanceSigs we allow the user to supply a signature for the
+method in an instance declaration.  Here is an artificial example:
+
+       data Age = MkAge Int
+       instance Ord Age where
+         compare :: a -> a -> Bool
+         compare = error "You can't compare Ages"
+
+The instance signature can be *more* polymorphic than the instantiated
+class method (in this case: Age -> Age -> Bool), but it cannot be less
+polymorphic.  Moreover, if a signature is given, the implementation
+code should match the signature, and type variables bound in the
+singature should scope over the method body.
+
+We achieve this by building a TcSigInfo for the method, whether or not
+there is an instance method signature, and using that to typecheck
+the declaration (in tcInstanceMethodBody).  That means, conveniently,
+that the type variables bound in the signature will scope over the body.
+
+What about the check that the instance method signature is more
+polymorphic than the instantiated class method type?  We just do a
+tcSubType call in mkMethIds, and use the HsWrapper thus generated in
+the method AbsBind.  It's very like the tcSubType impedence-matching
+call in mkExport.  We have to pass the HsWrapper into
+tcInstanceMethodBody.
+
+
 Note [Silent superclass arguments]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 See Trac #3731, #4809, #5751, #5913, #6117, which all
@@ -1201,15 +1223,16 @@ tcInstanceMethods dfun_id clas tyvars dfun_ev_vars inst_tys
     tc_body sig_fn sel_id rn_bind bndr_loc
       = add_meth_ctxt sel_id rn_bind $
         do { traceTc "tc_item" (ppr sel_id <+> ppr (idType sel_id))
-           ; (meth_id, local_meth_sig) <- setSrcSpan bndr_loc $
-                                          mkMethIds sig_fn clas tyvars dfun_ev_vars
-                                                    inst_tys sel_id
+           ; (meth_id, local_meth_sig, hs_wrap) 
+                  <- setSrcSpan bndr_loc $
+                     mkMethIds sig_fn clas tyvars dfun_ev_vars
+                               inst_tys sel_id
            ; let prags = prag_fn (idName sel_id)
            ; meth_id1 <- addInlinePrags meth_id prags
            ; spec_prags <- tcSpecPrags meth_id1 prags
            ; bind <- tcInstanceMethodBody InstSkol
                           tyvars dfun_ev_vars
-                          meth_id1 local_meth_sig
+                          meth_id1 local_meth_sig hs_wrap
                           (mk_meth_spec_prags meth_id1 spec_prags)
                           rn_bind
            ; return (meth_id1, bind) }
@@ -1223,8 +1246,8 @@ tcInstanceMethods dfun_id clas tyvars dfun_ev_vars inst_tys
 
     tc_default sig_fn sel_id NoDefMeth     -- No default method at all
       = do { traceTc "tc_def: warn" (ppr sel_id)
-           ; (meth_id, _) <- mkMethIds sig_fn clas tyvars dfun_ev_vars
-                                       inst_tys sel_id
+           ; (meth_id, _, _) <- mkMethIds sig_fn clas tyvars dfun_ev_vars
+                                          inst_tys sel_id
            ; dflags <- getDynFlags
            ; return (meth_id,
                      mkVarBind meth_id $
@@ -1239,7 +1262,7 @@ tcInstanceMethods dfun_id clas tyvars dfun_ev_vars inst_tys
         lam_wrapper  = mkWpTyLams tyvars <.> mkWpLams dfun_ev_vars
 
     tc_default sig_fn sel_id (DefMeth dm_name) -- A polymorphic default method
-      = do {   -- Build the typechecked version directly,
+      = do {     -- Build the typechecked version directly,
                  -- without calling typecheck_method;
                  -- see Note [Default methods in instances]
                  -- Generate   /\as.\ds. let self = df as ds
@@ -1251,8 +1274,8 @@ tcInstanceMethods dfun_id clas tyvars dfun_ev_vars inst_tys
            ; let self_ev_bind = EvBind self_dict
                                 (EvDFunApp dfun_id (mkTyVarTys tyvars) (map EvId dfun_ev_vars))
 
-           ; (meth_id, local_meth_sig) <- mkMethIds sig_fn clas tyvars dfun_ev_vars
-                                                    inst_tys sel_id
+           ; (meth_id, local_meth_sig, hs_wrap) 
+                   <- mkMethIds sig_fn clas tyvars dfun_ev_vars inst_tys sel_id
            ; dm_id <- tcLookupId dm_name
            ; let dm_inline_prag = idInlinePragma dm_id
                  rhs = HsWrap (mkWpEvVarApps [self_dict] <.> mkWpTyApps inst_tys) $
@@ -1265,7 +1288,7 @@ tcInstanceMethods dfun_id clas tyvars dfun_ev_vars inst_tys
                         -- method to this version. Note [INLINE and default methods]
 
 
-                 export = ABE { abe_wrap = idHsWrapper, abe_poly = meth_id1
+                 export = ABE { abe_wrap = hs_wrap, abe_poly = meth_id1
                               , abe_mono = local_meth_id
                               , abe_prags = mk_meth_spec_prags meth_id1 [] }
                  bind = AbsBinds { abs_tvs = tyvars, abs_ev_vars = dfun_ev_vars
index 586b31d..18809fd 100644 (file)
@@ -5313,7 +5313,7 @@ on the grounds that a later instance declaration might overlap the local one.)
 </sect3>
 
 <sect3 id="instance-sigs">
-<title>Type signatures in instance declarations</title>
+<title>Instance signatures: type signatures in instance declarations</title>
 <para>In Haskell, you can't write a type signature in an instance declaration, but it
 is sometimes convenient to do so, and the language extension <option>-XInstanceSigs</option>
 allows you to do so.  For example:
@@ -5323,10 +5323,30 @@ allows you to do so.  For example:
     (==) :: T a -> T a -> Bool   -- The signature
     (==) (MkT x1 x2) (MkTy y1 y2) = x1==y1 &amp;&amp; x2==y2
 </programlisting>
-The type signature in the instance declaration must be precisely the same as
+</para>
+Some details
+<itemizedlist>
+<listitem><para>
+The type signature in the instance declaration must be more polymorphic than (or the same as)
 the one in the class declaration, instantiated with the instance type.
+For example, this is fine:
+<programlisting>
+  instance Eq a => Eq (T a) where
+     (==) :: forall b. b -> b -> Bool
+     (==) x y = True
+</programlisting>
+Here the signature in the instance declaration is more polymorphic than that
+required by the instantiated class method.
 </para>
-<para>
+</listitem>
+
+<listitem><para>
+The code for the method in the instance declaration is typechecked against the type signature
+supplied in the instance declaration, as you would expect. So if the instance signature
+is more polymorphic than required, the code must be too.
+</para></listitem>
+
+<listitem><para>
 One stylistic reason for wanting to write a type signature is simple documentation.  Another
 is that you may want to bring scoped type variables into scope.  For example:
 <programlisting>
@@ -5344,7 +5364,8 @@ Provided that you also specify <option>-XScopedTypeVariables</option>
 (<xref linkend="scoped-type-variables"/>),
 the <literal>forall b</literal> scopes over the definition of <literal>foo</literal>,
 and in particular over the type signature for <literal>xs</literal>.
-</para>
+</para></listitem>
+</itemizedlist>
 </sect3>
 
 </sect2>
diff --git a/testsuite/tests/indexed-types/should_compile/T9582.hs b/testsuite/tests/indexed-types/should_compile/T9582.hs
new file mode 100644 (file)
index 0000000..f86d723
--- /dev/null
@@ -0,0 +1,14 @@
+{-# LANGUAGE InstanceSigs, TypeFamilies #-}
+module T9582 where
+
+class C a where
+  type T a
+  m :: T a
+
+instance C Int where
+  type T Int = String
+  m :: String
+  m = "bla"
+
+-- Method signature does not match class; it should be m :: T Int
+--    In the instance declaration for ‘C Int’
index fbd0b0e..4c48d3e 100644 (file)
@@ -249,3 +249,4 @@ test('red-black-delete', normal, compile, [''])
 test('Sock', normal, compile, [''])
 test('T9211', normal, compile, [''])
 test('T9747', normal, compile, [''])
+test('T9582', normal, compile, [''])
diff --git a/testsuite/tests/polykinds/T9833.hs b/testsuite/tests/polykinds/T9833.hs
new file mode 100644 (file)
index 0000000..0566256
--- /dev/null
@@ -0,0 +1,18 @@
+{-# LANGUAGE InstanceSigs, PolyKinds #-}
+
+module T9833 where
+
+import Control.Applicative
+
+data NullableInterp a = NullI Bool
+
+instance Functor     NullableInterp where
+  fmap = undefined
+instance Applicative NullableInterp where
+  pure  = undefined
+  (<*>) = undefined
+
+instance Alternative NullableInterp where
+  empty :: NullableInterp a
+  empty = undefined
+  (<|>) = undefined
\ No newline at end of file
index 19a194e..387e2bf 100644 (file)
@@ -112,3 +112,5 @@ test('T9750', normal, compile, [''])
 test('T9569', normal, compile, [''])
 test('T9838', normal, multimod_compile, ['T9838.hs','-v0'])
 test('T9574', normal, compile_fail, [''])
+test('T9833', normal, compile, [''])
+
index 593b43f..57d55dc 100644 (file)
@@ -1,5 +1,10 @@
 
 T6001.hs:8:18:
-    Method signature does not match class; it should be
-      fromInteger :: Integer -> DayKind
+    Couldn't match type ‘Integer’ with ‘Int’
+    Expected type: Integer -> DayKind
+      Actual type: Int -> DayKind
+    When checking that instance signature for ‘fromInteger’
+      is more general than its signature in the class
+      Instance sig: Int -> DayKind
+         Class sig: Integer -> DayKind
     In the instance declaration for ‘Num DayKind’
index 0acd4f8..614f665 100644 (file)
@@ -4,6 +4,7 @@ module T7545 where
 class C a where
    f :: a -> b
 
+-- This is now accepted because the instance signature is more general
 instance C (a -> b) where
    f :: x
    f = undefined
diff --git a/testsuite/tests/typecheck/should_fail/T7545.stderr b/testsuite/tests/typecheck/should_fail/T7545.stderr
deleted file mode 100644 (file)
index a1f2853..0000000
+++ /dev/null
@@ -1,5 +0,0 @@
-
-T7545.hs:8:9:
-    Method signature does not match class; it should be
-      f :: forall b1. (a -> b) -> b1
-    In the instance declaration for ‘C (a -> b)’
index 96c1908..7d1e558 100644 (file)
@@ -293,7 +293,7 @@ test('T7410', normal, compile_fail, [''])
 test('T7453', normal, compile_fail, [''])
 test('T7525', normal, compile_fail, [''])
 test('T7368a', normal, compile_fail, [''])
-test('T7545', normal, compile_fail, [''])
+test('T7545', normal, compile, [''])
 test('T7279', normal, compile_fail, [''])
 test('T2247', normal, compile_fail, [''])
 test('T7609', normal, compile_fail, [''])