Add valid refinement substitution suggestions for typed holes
[ghc.git] / compiler / typecheck / TcSigs.hs
index e26133e..62fa832 100644 (file)
@@ -5,6 +5,7 @@
 -}
 
 {-# LANGUAGE CPP #-}
+{-# LANGUAGE TypeFamilies #-}
 
 module TcSigs(
        TcSigInfo(..),
@@ -12,7 +13,7 @@ module TcSigs(
        TcPatSynInfo(..),
        TcSigFun,
 
-       isPartialSig, noCompleteSig, tcIdSigName, tcSigInfoName,
+       isPartialSig, hasCompleteSig, tcIdSigName, tcSigInfoName,
        completeSigPolyId_maybe,
 
        tcTySigs, tcUserTypeSig, completeSigFromId,
@@ -24,6 +25,8 @@ module TcSigs(
 
 #include "HsVersions.h"
 
+import GhcPrelude
+
 import HsSyn
 import TcHsType
 import TcRnTypes
@@ -31,7 +34,7 @@ import TcRnMonad
 import TcType
 import TcMType
 import TcValidity ( checkValidType )
-import TcUnify( tcSkolemise, unifyType, noThing )
+import TcUnify( tcSkolemise, unifyType )
 import Inst( topInstantiate )
 import TcEnv( tcLookupId )
 import TcEvidence( HsWrapper, (<.>) )
@@ -143,13 +146,6 @@ errors were dealt with by the renamer.
 *                                                                      *
 ********************************************************************* -}
 
-type TcSigFun  = Name -> Maybe TcSigInfo
-
--- | No signature or a partial signature
-noCompleteSig :: Maybe TcSigInfo -> Bool
-noCompleteSig (Just (TcIdSig (CompleteSig {}))) = False
-noCompleteSig _                                 = True
-
 tcIdSigName :: TcIdSigInfo -> Name
 tcIdSigName (CompleteSig { sig_bndr = id }) = idName id
 tcIdSigName (PartialSig { psig_name = n })  = n
@@ -171,7 +167,7 @@ completeSigPolyId_maybe sig
 *                                                                      *
 ********************************************************************* -}
 
-tcTySigs :: [LSig Name] -> TcM ([TcId], TcSigFun)
+tcTySigs :: [LSig GhcRn] -> TcM ([TcId], TcSigFun)
 tcTySigs hs_sigs
   = checkNoErrs $   -- See Note [Fail eagerly on bad signatures]
     do { ty_sigs_s <- mapAndRecoverM tcTySig hs_sigs
@@ -183,7 +179,7 @@ tcTySigs hs_sigs
              env = mkNameEnv [(tcSigInfoName sig, sig) | sig <- ty_sigs]
        ; return (poly_ids, lookupNameEnv env) }
 
-tcTySig :: LSig Name -> TcM [TcSigInfo]
+tcTySig :: LSig GhcRn -> TcM [TcSigInfo]
 tcTySig (L _ (IdSig id))
   = do { let ctxt = FunSigCtxt (idName id) False
                     -- False: do not report redundant constraints
@@ -206,7 +202,8 @@ tcTySig (L loc (PatSynSig names sig_ty))
 tcTySig _ = return []
 
 
-tcUserTypeSig :: SrcSpan -> LHsSigWcType Name -> Maybe Name -> TcM TcIdSigInfo
+tcUserTypeSig :: SrcSpan -> LHsSigWcType GhcRn -> Maybe Name
+              -> TcM TcIdSigInfo
 -- A function or expression type signature
 -- Returns a fully quantified type signature; even the wildcards
 -- are quantified with ordinary skolems that should be instantiated
@@ -251,7 +248,7 @@ completeSigFromId ctxt id
                 , sig_ctxt = ctxt
                 , sig_loc  = getSrcSpan id }
 
-isCompleteHsSig :: LHsSigWcType Name -> Bool
+isCompleteHsSig :: LHsSigWcType GhcRn -> Bool
 -- ^ If there are no wildcards, return a LHsSigType
 isCompleteHsSig (HsWC { hswc_wcs = wcs }) = null wcs
 
@@ -292,57 +289,16 @@ Once we get to type checking, we decompose it into its parts, in tcPatSynSig.
 
 * Note that 'forall univ_tvs' and 'req_theta =>'
         and 'forall ex_tvs'   and 'prov_theta =>'
-  are all optional.  We gather the pieces at the the top of tcPatSynSig
+  are all optional.  We gather the pieces at the top of tcPatSynSig
 
 * Initially the implicitly-bound tyvars (added by the renamer) include both
   universal and existential vars.
 
 * After we kind-check the pieces and convert to Types, we do kind generalisation.
-
-Note [The pattern-synonym signature splitting rule]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Given a pattern signature, we must split
-     the kind-generalised variables, and
-     the implicitly-bound variables
-into universal and existential.  The rule is this
-(see discussion on Trac #11224):
-
-     The universal tyvars are the ones mentioned in
-          - univ_tvs: the user-specified (forall'd) universals
-          - req_theta
-          - res_ty
-     The existential tyvars are all the rest
-
-For example
-
-   pattern P :: () => b -> T a
-   pattern P x = ...
-
-Here 'a' is universal, and 'b' is existential.  But there is a wrinkle:
-how do we split the arg_tys from req_ty?  Consider
-
-   pattern Q :: () => b -> S c -> T a
-   pattern Q x = ...
-
-This is an odd example because Q has only one syntactic argument, and
-so presumably is defined by a view pattern matching a function.  But
-it can happen (Trac #11977, #12108).
-
-We don't know Q's arity from the pattern signature, so we have to wait
-until we see the pattern declaration itself before deciding res_ty is,
-and hence which variables are existential and which are universal.
-
-And that in turn is why TcPatSynInfo has a separate field,
-patsig_implicit_bndrs, to capture the implicitly bound type variables,
-because we don't yet know how to split them up.
-
-It's a slight compromise, because it means we don't really know the
-pattern synonym's real signature until we see its declaration.  So,
-for example, in hs-boot file, we may need to think what to do...
-(eg don't have any implicitly-bound variables).
 -}
 
-tcPatSynSig :: Name -> LHsSigType Name -> TcM TcPatSynInfo
+tcPatSynSig :: Name -> LHsSigType GhcRn -> TcM TcPatSynInfo
+-- See Note [Pattern synonym signatures]
 tcPatSynSig name sig_ty
   | HsIB { hsib_vars = implicit_hs_tvs
          , hsib_body = hs_ty }  <- sig_ty
@@ -449,12 +405,30 @@ tcInstSig sig@(PartialSig { psig_hs_ty = hs_ty
                           , sig_loc = loc })
   = setSrcSpan loc $  -- Set the binding site of the tyvars
     do { (wcs, wcx, tvs, theta, tau) <- tcHsPartialSigType ctxt hs_ty
+
+        -- Clone the quantified tyvars
+        -- Reason: we might have    f, g :: forall a. a -> _ -> a
+        --         and we want it to behave exactly as if there were
+        --         two separate signatures.  Cloning here seems like
+        --         the easiest way to do so, and is very similar to
+        --         the tcInstType in the CompleteSig case
+        -- See Trac #14643
+        ; (subst, tvs') <- instSkolTyCoVars mk_sig_tv tvs
+        ; let tv_prs = map tyVarName tvs `zip` tvs'
+
        ; return (TISI { sig_inst_sig   = sig
-                      , sig_inst_skols = map (\tv -> (tyVarName tv, tv)) tvs
+                      , sig_inst_skols = tv_prs
                       , sig_inst_wcs   = wcs
                       , sig_inst_wcx   = wcx
-                      , sig_inst_theta = theta
-                      , sig_inst_tau   = tau }) }
+                      , sig_inst_theta = substTys subst theta
+                      , sig_inst_tau   = substTy  subst tau
+                }) }
+  where
+    mk_sig_tv old_name kind
+      = do { uniq <- newUnique
+           ; newSigTyVar (setNameUnique old_name uniq) kind }
+      -- Why newSigTyVar?  See TcBinds
+      -- Note [Quantified variables in partial type signatures]
 
 
 {- Note [Pattern bindings and complete signatures]
@@ -470,7 +444,7 @@ the signature types for f and g, we'll end up unifying 'a' and 'b'
 So we instantiate f and g's signature with SigTv skolems
 (newMetaSigTyVars) that can unify with each other.  If too much
 unification takes place, we'll find out when we do the final
-impedence-matching check in TcBinds.mkExport
+impedance-matching check in TcBinds.mkExport
 
 See Note [Signature skolems] in TcType
 
@@ -484,25 +458,25 @@ signature, which doesn't use tcInstSig.  See TcBinds.tcPolyCheck.
 *                                                                      *
 ********************************************************************* -}
 
-type TcPragEnv = NameEnv [LSig Name]
+type TcPragEnv = NameEnv [LSig GhcRn]
 
 emptyPragEnv :: TcPragEnv
 emptyPragEnv = emptyNameEnv
 
-lookupPragEnv :: TcPragEnv -> Name -> [LSig Name]
+lookupPragEnv :: TcPragEnv -> Name -> [LSig GhcRn]
 lookupPragEnv prag_fn n = lookupNameEnv prag_fn n `orElse` []
 
-extendPragEnv :: TcPragEnv -> (Name, LSig Name) -> TcPragEnv
+extendPragEnv :: TcPragEnv -> (Name, LSig GhcRn) -> TcPragEnv
 extendPragEnv prag_fn (n, sig) = extendNameEnv_Acc (:) singleton prag_fn n sig
 
 ---------------
-mkPragEnv :: [LSig Name] -> LHsBinds Name -> TcPragEnv
+mkPragEnv :: [LSig GhcRn] -> LHsBinds GhcRn -> TcPragEnv
 mkPragEnv sigs binds
   = foldl extendPragEnv emptyNameEnv prs
   where
     prs = mapMaybe get_sig sigs
 
-    get_sig :: LSig Name -> Maybe (Name, LSig Name)
+    get_sig :: LSig GhcRn -> Maybe (Name, LSig GhcRn)
     get_sig (L l (SpecSig lnm@(L _ nm) ty inl)) = Just (nm, L l $ SpecSig   lnm ty (add_arity nm inl))
     get_sig (L l (InlineSig lnm@(L _ nm) inl))  = Just (nm, L l $ InlineSig lnm    (add_arity nm inl))
     get_sig (L l (SCCFunSig st lnm@(L _ nm) str))  = Just (nm, L l $ SCCFunSig st lnm str)
@@ -523,14 +497,14 @@ mkPragEnv sigs binds
     ar_env :: NameEnv Arity
     ar_env = foldrBag lhsBindArity emptyNameEnv binds
 
-lhsBindArity :: LHsBind Name -> NameEnv Arity -> NameEnv Arity
+lhsBindArity :: LHsBind GhcRn -> NameEnv Arity -> NameEnv Arity
 lhsBindArity (L _ (FunBind { fun_id = id, fun_matches = ms })) env
   = extendNameEnv env (unLoc id) (matchGroupArity ms)
 lhsBindArity _ env = env        -- PatBind/VarBind
 
 
 -----------------
-addInlinePrags :: TcId -> [LSig Name] -> TcM TcId
+addInlinePrags :: TcId -> [LSig GhcRn] -> TcM TcId
 addInlinePrags poly_id prags_for_me
   | inl@(L _ prag) : inls <- inl_prags
   = do { traceTc "addInlinePrag" (ppr poly_id $$ ppr prag)
@@ -545,7 +519,7 @@ addInlinePrags poly_id prags_for_me
 
     warn_multiple_inlines inl1@(L loc prag1) (inl2@(L _ prag2) : inls)
        | inlinePragmaActivation prag1 == inlinePragmaActivation prag2
-       , isEmptyInlineSpec (inlinePragmaSpec prag1)
+       , noUserInlineSpec (inlinePragmaSpec prag1)
        =    -- Tiresome: inl1 is put there by virtue of being in a hs-boot loop
             -- and inl2 is a user NOINLINE pragma; we don't want to complain
          warn_multiple_inlines inl2 inls
@@ -667,7 +641,7 @@ Some wrinkles
    well as the dict.  That's what goes on in TcInstDcls.mk_meth_spec_prags
 -}
 
-tcSpecPrags :: Id -> [LSig Name]
+tcSpecPrags :: Id -> [LSig GhcRn]
             -> TcM [LTcSpecPrag]
 -- Add INLINE and SPECIALSE pragmas
 --    INLINE prags are added to the (polymorphic) Id directly
@@ -690,7 +664,7 @@ tcSpecPrags poly_id prag_sigs
                       2 (vcat (map (ppr . getLoc) bad_sigs)))
 
 --------------
-tcSpecPrag :: TcId -> Sig Name -> TcM [TcSpecPrag]
+tcSpecPrag :: TcId -> Sig GhcRn -> TcM [TcSpecPrag]
 tcSpecPrag poly_id prag@(SpecSig fun_name hs_tys inl)
 -- See Note [Handling SPECIALISE pragmas]
 --
@@ -700,7 +674,7 @@ tcSpecPrag poly_id prag@(SpecSig fun_name hs_tys inl)
 -- However we want to use fun_name in the error message, since that is
 -- what the user wrote (Trac #8537)
   = addErrCtxt (spec_ctxt prag) $
-    do  { warnIf NoReason (not (isOverloadedTy poly_ty || isInlinePragma inl))
+    do  { warnIf (not (isOverloadedTy poly_ty || isInlinePragma inl))
                  (text "SPECIALISE pragma for non-overloaded function"
                   <+> quotes (ppr fun_name))
                   -- Note [SPECIALISE pragmas]
@@ -727,7 +701,7 @@ tcSpecWrapper ctxt poly_ty spec_ty
   = do { (sk_wrap, inst_wrap)
                <- tcSkolemise ctxt spec_ty $ \ _ spec_tau ->
                   do { (inst_wrap, tau) <- topInstantiate orig poly_ty
-                     ; _ <- unifyType noThing spec_tau tau
+                     ; _ <- unifyType Nothing spec_tau tau
                             -- Deliberately ignore the evidence
                             -- See Note [Handling SPECIALISE pragmas],
                             --   wrinkle (2)
@@ -737,7 +711,7 @@ tcSpecWrapper ctxt poly_ty spec_ty
     orig = SpecPragOrigin ctxt
 
 --------------
-tcImpPrags :: [LSig Name] -> TcM [LTcSpecPrag]
+tcImpPrags :: [LSig GhcRn] -> TcM [LTcSpecPrag]
 -- SPECIALISE pragmas for imported things
 tcImpPrags prags
   = do { this_mod <- getModule
@@ -754,7 +728,7 @@ tcImpPrags prags
     -- Ignore SPECIALISE pragmas for imported things
     -- when we aren't specialising, or when we aren't generating
     -- code.  The latter happens when Haddocking the base library;
-    -- we don't wnat complaints about lack of INLINABLE pragmas
+    -- we don't want complaints about lack of INLINABLE pragmas
     not_specialising dflags
       | not (gopt Opt_Specialise dflags) = True
       | otherwise = case hscTarget dflags of
@@ -762,7 +736,7 @@ tcImpPrags prags
                       HscInterpreted -> True
                       _other         -> False
 
-tcImpSpec :: (Name, Sig Name) -> TcM [TcSpecPrag]
+tcImpSpec :: (Name, Sig GhcRn) -> TcM [TcSpecPrag]
 tcImpSpec (name, prag)
  = do { id <- tcLookupId name
       ; unless (isAnyInlinePragma (idInlinePragma id))