Fix #14934 by including axSub0R in typeNatCoAxiomRules
[ghc.git] / compiler / iface / TcIface.hs
index 2a56392..ca1a17d 100644 (file)
@@ -15,13 +15,15 @@ module TcIface (
         typecheckIfacesForMerging,
         typecheckIfaceForInstantiate,
         tcIfaceDecl, tcIfaceInst, tcIfaceFamInst, tcIfaceRules,
-        tcIfaceVectInfo, tcIfaceAnnotations,
+        tcIfaceVectInfo, tcIfaceAnnotations, tcIfaceCompleteSigs,
         tcIfaceExpr,    -- Desired by HERMIT (Trac #7683)
         tcIfaceGlobal
  ) where
 
 #include "HsVersions.h"
 
+import GhcPrelude
+
 import TcTypeNats(typeNatCoAxiomRules)
 import IfaceSyn
 import LoadIface
@@ -255,7 +257,7 @@ mergeIfaceDecl d1 d2
 --
 -- A module that defines T as representational in both arguments
 -- would successfully fill both signatures, so it would be better
--- if if we merged the roles of these types in some nontrivial
+-- if we merged the roles of these types in some nontrivial
 -- way.
 --
 -- However, we have to be very careful about how we go about
@@ -645,7 +647,7 @@ tc_iface_decl _ ignore_prags (IfaceId {ifName = name, ifType = iface_type,
                                        ifIdDetails = details, ifIdInfo = info})
   = do  { ty <- tcIfaceType iface_type
         ; details <- tcIdDetails ty details
-        ; info <- tcIdInfo ignore_prags name ty info
+        ; info <- tcIdInfo ignore_prags TopLevel name ty info
         ; return (AnId (mkGlobalId details name ty info)) }
 
 tc_iface_decl _ _ (IfaceData {ifName = tc_name,
@@ -807,7 +809,14 @@ tc_iface_decl _parent ignore_prags
 tc_iface_decl _ _ (IfaceAxiom { ifName = tc_name, ifTyCon = tc
                               , ifAxBranches = branches, ifRole = role })
   = do { tc_tycon    <- tcIfaceTyCon tc
-       ; tc_branches <- tc_ax_branches branches
+       -- Must be done lazily, because axioms are forced when checking
+       -- for family instance consistency, and the RHS may mention
+       -- a hs-boot declared type constructor that is going to be
+       -- defined by this module.
+       -- e.g. type instance F Int = ToBeDefined
+       -- See Trac #13803
+       ; tc_branches <- forkM (text "Axiom branches" <+> ppr tc_name)
+                      $ tc_ax_branches branches
        ; let axiom = CoAxiom { co_ax_unique   = nameUnique tc_name
                              , co_ax_name     = tc_name
                              , co_ax_tc       = tc_tycon
@@ -885,11 +894,15 @@ tcIfaceDataCons tycon_name tycon tc_tybinders if_cons
         IfNewTyCon  con  -> do  { data_con  <- tc_con_decl con
                                 ; mkNewTyConRhs tycon_name tycon data_con }
   where
-    univ_tv_bndrs :: [TyVarBinder]
-    univ_tv_bndrs = mkDataConUnivTyVarBinders tc_tybinders
+    univ_tvs :: [TyVar]
+    univ_tvs = binderVars (tyConTyVarBinders tc_tybinders)
+
+    tag_map :: NameEnv ConTag
+    tag_map = mkTyConTagMap tycon
 
     tc_con_decl (IfCon { ifConInfix = is_infix,
                          ifConExTvs = ex_bndrs,
+                         ifConUserTvBinders = user_bndrs,
                          ifConName = dc_name,
                          ifConCtxt = ctxt, ifConEqSpec = spec,
                          ifConArgTys = args, ifConFields = lbl_names,
@@ -897,9 +910,19 @@ tcIfaceDataCons tycon_name tycon tc_tybinders if_cons
                          ifConSrcStricts = if_src_stricts})
      = -- Universally-quantified tyvars are shared with
        -- parent TyCon, and are already in scope
-       bindIfaceForAllBndrs ex_bndrs    $ \ ex_tv_bndrs -> do
+       bindIfaceTyVars ex_bndrs    $ \ ex_tvs -> do
         { traceIf (text "Start interface-file tc_con_decl" <+> ppr dc_name)
 
+          -- By this point, we have bound every universal and existential
+          -- tyvar. Because of the dcUserTyVarBinders invariant
+          -- (see Note [DataCon user type variable binders]), *every* tyvar in
+          -- ifConUserTvBinders has a matching counterpart somewhere in the
+          -- bound universals/existentials. As a result, calling tcIfaceTyVar
+          -- below is always guaranteed to succeed.
+        ; user_tv_bndrs <- mapM (\(TvBndr (name, _) vis) ->
+                                    TvBndr <$> tcIfaceTyVar name <*> pure vis)
+                                user_bndrs
+
         -- Read the context and argument types, but lazily for two reasons
         -- (a) to avoid looking tugging on a recursive use of
         --     the type itself, which is knot-tied
@@ -908,7 +931,14 @@ tcIfaceDataCons tycon_name tycon tc_tybinders if_cons
         ; ~(eq_spec, theta, arg_tys, stricts) <- forkM (mk_doc dc_name) $
              do { eq_spec <- tcIfaceEqSpec spec
                 ; theta   <- tcIfaceCtxt ctxt
-                ; arg_tys <- mapM tcIfaceType args
+                -- This fixes #13710.  The enclosing lazy thunk gets
+                -- forced when typechecking record wildcard pattern
+                -- matching (it's not completely clear why this
+                -- tuple is needed), which causes trouble if one of
+                -- the argument types was recursively defined.
+                -- See also Note [Tying the knot]
+                ; arg_tys <- forkM (mk_doc dc_name <+> text "arg_tys")
+                           $ mapM tcIfaceType args
                 ; stricts <- mapM tc_strict if_stricts
                         -- The IfBang field can mention
                         -- the type itself; hence inside forkM
@@ -931,9 +961,9 @@ tcIfaceDataCons tycon_name tycon tc_tybinders if_cons
                        -- worker.
                        -- See Note [Bangs on imported data constructors] in MkId
                        lbl_names
-                       univ_tv_bndrs ex_tv_bndrs
+                       univ_tvs ex_tvs user_tv_bndrs
                        eq_spec theta
-                       arg_tys orig_res_ty tycon
+                       arg_tys orig_res_ty tycon tag_map
         ; traceIf (text "Done interface-file tc_con_decl" <+> ppr dc_name)
         ; return con }
     mk_doc con_name = text "Constructor" <+> ppr con_name
@@ -1096,9 +1126,7 @@ tcIfaceCompleteSigs :: [IfaceCompleteMatch] -> IfL [CompleteMatch]
 tcIfaceCompleteSigs = mapM tcIfaceCompleteSig
 
 tcIfaceCompleteSig :: IfaceCompleteMatch -> IfL CompleteMatch
-tcIfaceCompleteSig cm@(IfaceCompleteMatch ms t) =
-  forkM (text "COMPLETE" <+> ppr cm) $
-    CompleteMatch <$> mapM tcIfaceConLike ms <*> tcIfaceTyConByName t
+tcIfaceCompleteSig (IfaceCompleteMatch ms t) = return (CompleteMatch ms t)
 
 {-
 ************************************************************************
@@ -1331,25 +1359,19 @@ tcIfaceCo = go
                                                <*> go c2
     go (IfaceKindCo c)           = KindCo   <$> go c
     go (IfaceSubCo c)            = SubCo    <$> go c
-    go (IfaceAxiomRuleCo ax cos) = AxiomRuleCo <$> go_axiom_rule ax
+    go (IfaceAxiomRuleCo ax cos) = AxiomRuleCo <$> tcIfaceCoAxiomRule ax
                                                <*> mapM go cos
+    go (IfaceFreeCoVar c)        = pprPanic "tcIfaceCo:IfaceFreeCoVar" (ppr c)
+    go (IfaceHoleCo c)           = pprPanic "tcIfaceCo:IfaceHoleCo"    (ppr c)
 
     go_var :: FastString -> IfL CoVar
     go_var = tcIfaceLclId
 
-    go_axiom_rule :: FastString -> IfL CoAxiomRule
-    go_axiom_rule n =
-      case Map.lookup n typeNatCoAxiomRules of
-        Just ax -> return ax
-        _  -> pprPanic "go_axiom_rule" (ppr n)
-
 tcIfaceUnivCoProv :: IfaceUnivCoProv -> IfL UnivCoProvenance
 tcIfaceUnivCoProv IfaceUnsafeCoerceProv     = return UnsafeCoerceProv
 tcIfaceUnivCoProv (IfacePhantomProv kco)    = PhantomProv <$> tcIfaceCo kco
 tcIfaceUnivCoProv (IfaceProofIrrelProv kco) = ProofIrrelProv <$> tcIfaceCo kco
 tcIfaceUnivCoProv (IfacePluginProv str)     = return $ PluginProv str
-tcIfaceUnivCoProv (IfaceHoleProv _)         =
-    pprPanic "tcIfaceUnivCoProv" (text "holes can't occur in interface files")
 
 {-
 ************************************************************************
@@ -1391,7 +1413,7 @@ tcIfaceExpr (IfaceTuple sort args)
        ; let con_tys = map exprType args'
              some_con_args = map Type con_tys ++ args'
              con_args = case sort of
-               UnboxedTuple -> map (Type . getRuntimeRep "tcIfaceExpr") con_tys ++ some_con_args
+               UnboxedTuple -> map (Type . getRuntimeRep) con_tys ++ some_con_args
                _            -> some_con_args
                         -- Put the missing type arguments back in
              con_id   = dataConWorkId (tyConSingleDataCon tc)
@@ -1435,7 +1457,7 @@ tcIfaceExpr (IfaceLet (IfaceNonRec (IfLetBndr fs ty info ji) rhs) body)
   = do  { name    <- newIfaceName (mkVarOccFS fs)
         ; ty'     <- tcIfaceType ty
         ; id_info <- tcIdInfo False {- Don't ignore prags; we are inside one! -}
-                              name ty' info
+                              NotTopLevel name ty' info
         ; let id = mkLocalIdOrCoVarWithInfo name ty' id_info
                      `asJoinId_maybe` tcJoinInfo ji
         ; rhs' <- tcIfaceExpr rhs
@@ -1456,7 +1478,7 @@ tcIfaceExpr (IfaceLet (IfaceRec pairs) body)
    tc_pair (IfLetBndr _ _ info _, rhs) id
      = do { rhs' <- tcIfaceExpr rhs
           ; id_info <- tcIdInfo False {- Don't ignore prags; we are inside one! -}
-                                (idName id) (idType id) info
+                                NotTopLevel (idName id) (idType id) info
           ; return (setIdInfo id id_info, rhs') }
 
 tcIfaceExpr (IfaceTick tickish expr) = do
@@ -1547,8 +1569,8 @@ tcIdDetails _ (IfRecSelId tc naughty)
     tyThingPatSyn (AConLike (PatSynCon ps)) = ps
     tyThingPatSyn _ = panic "tcIdDetails: expecting patsyn"
 
-tcIdInfo :: Bool -> Name -> Type -> IfaceIdInfo -> IfL IdInfo
-tcIdInfo ignore_prags name ty info = do
+tcIdInfo :: Bool -> TopLevelFlag -> Name -> Type -> IfaceIdInfo -> IfL IdInfo
+tcIdInfo ignore_prags toplvl name ty info = do
     lcl_env <- getLclEnv
     -- Set the CgInfo to something sensible but uninformative before
     -- we start; default assumption is that it has CAFs
@@ -1569,7 +1591,7 @@ tcIdInfo ignore_prags name ty info = do
 
         -- The next two are lazy, so they don't transitively suck stuff in
     tcPrag info (HsUnfold lb if_unf)
-      = do { unf <- tcUnfolding name ty info if_unf
+      = do { unf <- tcUnfolding toplvl name ty info if_unf
            ; let info1 | lb        = info `setOccInfo` strongLoopBreaker
                        | otherwise = info
            ; return (info1 `setUnfoldingInfo` unf) }
@@ -1578,10 +1600,10 @@ tcJoinInfo :: IfaceJoinInfo -> Maybe JoinArity
 tcJoinInfo (IfaceJoinPoint ar) = Just ar
 tcJoinInfo IfaceNotJoinPoint   = Nothing
 
-tcUnfolding :: Name -> Type -> IdInfo -> IfaceUnfolding -> IfL Unfolding
-tcUnfolding name _ info (IfCoreUnfold stable if_expr)
+tcUnfolding :: TopLevelFlag -> Name -> Type -> IdInfo -> IfaceUnfolding -> IfL Unfolding
+tcUnfolding toplvl name _ info (IfCoreUnfold stable if_expr)
   = do  { dflags <- getDynFlags
-        ; mb_expr <- tcPragExpr name if_expr
+        ; mb_expr <- tcPragExpr toplvl name if_expr
         ; let unf_src | stable    = InlineStable
                       | otherwise = InlineRhs
         ; return $ case mb_expr of
@@ -1594,21 +1616,21 @@ tcUnfolding name _ info (IfCoreUnfold stable if_expr)
   where
      -- Strictness should occur before unfolding!
     strict_sig = strictnessInfo info
-tcUnfolding name _ _ (IfCompulsory if_expr)
-  = do  { mb_expr <- tcPragExpr name if_expr
+tcUnfolding toplvl name _ _ (IfCompulsory if_expr)
+  = do  { mb_expr <- tcPragExpr toplvl name if_expr
         ; return (case mb_expr of
                     Nothing   -> NoUnfolding
                     Just expr -> mkCompulsoryUnfolding expr) }
 
-tcUnfolding name _ _ (IfInlineRule arity unsat_ok boring_ok if_expr)
-  = do  { mb_expr <- tcPragExpr name if_expr
+tcUnfolding toplvl name _ _ (IfInlineRule arity unsat_ok boring_ok if_expr)
+  = do  { mb_expr <- tcPragExpr toplvl name if_expr
         ; return (case mb_expr of
                     Nothing   -> NoUnfolding
                     Just expr -> mkCoreUnfolding InlineStable True expr guidance )}
   where
     guidance = UnfWhen { ug_arity = arity, ug_unsat_ok = unsat_ok, ug_boring_ok = boring_ok }
 
-tcUnfolding name dfun_ty _ (IfDFunUnfold bs ops)
+tcUnfolding _toplvl name dfun_ty _ (IfDFunUnfold bs ops)
   = bindIfaceBndrs bs $ \ bs' ->
     do { mb_ops1 <- forkM_maybe doc $ mapM tcIfaceExpr ops
        ; return (case mb_ops1 of
@@ -1623,13 +1645,14 @@ For unfoldings we try to do the job lazily, so that we never type check
 an unfolding that isn't going to be looked at.
 -}
 
-tcPragExpr :: Name -> IfaceExpr -> IfL (Maybe CoreExpr)
-tcPragExpr name expr
+tcPragExpr :: TopLevelFlag -> Name -> IfaceExpr -> IfL (Maybe CoreExpr)
+tcPragExpr toplvl name expr
   = forkM_maybe doc $ do
     core_expr' <- tcIfaceExpr expr
 
-                -- Check for type consistency in the unfolding
-    whenGOptM Opt_DoCoreLinting $ do
+    -- Check for type consistency in the unfolding
+    -- See Note [Linting Unfoldings from Interfaces]
+    when (isTopLevel toplvl) $ whenGOptM Opt_DoCoreLinting $ do
         in_scope <- get_in_scope
         dflags   <- getDynFlags
         case lintUnfolding dflags noSrcLoc in_scope core_expr' of
@@ -1687,13 +1710,13 @@ tcIfaceGlobal name
                 { type_env <- setLclEnv () get_type_env         -- yuk
                 ; case lookupNameEnv type_env name of
                     Just thing -> return thing
-                    Nothing   ->
-                      pprPanic "tcIfaceGlobal (local): not found"
-                               (ifKnotErr name (if_doc env) type_env)
+                    -- See Note [Knot-tying fallback on boot]
+                    Nothing   -> via_external
                 }
 
-          ; _ -> do
-
+          ; _ -> via_external }}
+  where
+    via_external =  do
         { hsc_env <- getTopEnv
         ; mb_thing <- liftIO (lookupTypeHscEnv hsc_env name)
         ; case mb_thing of {
@@ -1704,21 +1727,7 @@ tcIfaceGlobal name
         ; case mb_thing of
             Failed err      -> failIfM err
             Succeeded thing -> return thing
-    }}}}}
-
-ifKnotErr :: Name -> SDoc -> TypeEnv -> SDoc
-ifKnotErr name env_doc type_env = vcat
-  [ text "You are in a maze of twisty little passages, all alike."
-  , text "While forcing the thunk for TyThing" <+> ppr name
-  , text "which was lazily initialized by" <+> env_doc <> text ","
-  , text "I tried to tie the knot, but I couldn't find" <+> ppr name
-  , text "in the current type environment."
-  , text "If you are developing GHC, please read Note [Tying the knot]"
-  , text "and Note [Type-checking inside the knot]."
-  , text "Consider rebuilding GHC with profiling for a better stack trace."
-  , hang (text "Contents of current type environment:")
-       2 (ppr type_env)
-  ]
+        }}}
 
 -- Note [Tying the knot]
 -- ~~~~~~~~~~~~~~~~~~~~~
@@ -1733,11 +1742,50 @@ ifKnotErr name env_doc type_env = vcat
 --      * Note [Knot-tying typecheckIface]
 --      * Note [DFun knot-tying]
 --      * Note [hsc_type_env_var hack]
+--      * Note [Knot-tying fallback on boot]
 --
 -- There is also a wiki page on the subject, see:
 --
 --      https://ghc.haskell.org/trac/ghc/wiki/Commentary/Compiler/TyingTheKnot
 
+-- Note [Knot-tying fallback on boot]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-- Suppose that you are typechecking A.hs, which transitively imports,
+-- via B.hs, A.hs-boot. When we poke on B.hs and discover that it
+-- has a reference to a type T from A, what TyThing should we wire
+-- it up with? Clearly, if we have already typechecked T and
+-- added it into the type environment, we should go ahead and use that
+-- type. But what if we haven't typechecked it yet?
+--
+-- For the longest time, GHC adopted the policy that this was
+-- *an error condition*; that you MUST NEVER poke on B.hs's reference
+-- to a T defined in A.hs until A.hs has gotten around to kind-checking
+-- T and adding it to the env. However, actually ensuring this is the
+-- case has proven to be a bug farm, because it's really difficult to
+-- actually ensure this never happens. The problem was especially poignant
+-- with type family consistency checks, which eagerly happen before any
+-- typechecking takes place.
+--
+-- Today, we take a different strategy: if we ever try to access
+-- an entity from A which doesn't exist, we just fall back on the
+-- definition of A from the hs-boot file. This is complicated in
+-- its own way: it means that you may end up with a mix of A.hs and
+-- A.hs-boot TyThings during the course of typechecking.  We don't
+-- think (and have not observed) any cases where this would cause
+-- problems, but the hypothetical situation one might worry about
+-- is something along these lines in Core:
+--
+--    case x of
+--        A -> e1
+--        B -> e2
+--
+-- If, when typechecking this, we find x :: T, and the T we are hooked
+-- up with is the abstract one from the hs-boot file, rather than the
+-- one defined in this module with constructors A and B.  But it's hard
+-- to see how this could happen, especially because the reference to
+-- the constructor (A and B) means that GHC will always typecheck
+-- this expression *after* typechecking T.
+
 tcIfaceTyConByName :: IfExtName -> IfL TyCon
 tcIfaceTyConByName name
   = do { thing <- tcIfaceGlobal name
@@ -1754,20 +1802,22 @@ tcIfaceCoAxiom :: Name -> IfL (CoAxiom Branched)
 tcIfaceCoAxiom name = do { thing <- tcIfaceImplicit name
                          ; return (tyThingCoAxiom thing) }
 
+
+tcIfaceCoAxiomRule :: IfLclName -> IfL CoAxiomRule
+-- Unlike CoAxioms, which arise form user 'type instance' declarations,
+-- there are a fixed set of CoAxiomRules,
+-- currently enumerated in typeNatCoAxiomRules
+tcIfaceCoAxiomRule n
+  = case Map.lookup n typeNatCoAxiomRules of
+        Just ax -> return ax
+        _  -> pprPanic "tcIfaceCoAxiomRule" (ppr n)
+
 tcIfaceDataCon :: Name -> IfL DataCon
 tcIfaceDataCon name = do { thing <- tcIfaceGlobal name
                          ; case thing of
                                 AConLike (RealDataCon dc) -> return dc
                                 _       -> pprPanic "tcIfaceExtDC" (ppr name$$ ppr thing) }
 
-tcIfaceConLike :: Name -> IfL ConLike
-tcIfaceConLike name =
-    do { thing <- tcIfaceGlobal name
-       ; case thing of
-        AConLike cl -> return cl
-        _           -> pprPanic "tcIfaceExtCL" (ppr name$$ ppr thing) }
-
-
 tcIfaceExtId :: Name -> IfL Id
 tcIfaceExtId name = do { thing <- tcIfaceGlobal name
                        ; case thing of
@@ -1832,6 +1882,13 @@ bindIfaceForAllBndr :: IfaceForAllBndr -> (TyVar -> ArgFlag -> IfL a) -> IfL a
 bindIfaceForAllBndr (TvBndr tv vis) thing_inside
   = bindIfaceTyVar tv $ \tv' -> thing_inside tv' vis
 
+bindIfaceTyVars :: [IfaceTvBndr] -> ([TyVar] -> IfL a) -> IfL a
+bindIfaceTyVars [] thing_inside = thing_inside []
+bindIfaceTyVars (tv:tvs) thing_inside
+  = bindIfaceTyVar tv   $ \tv' ->
+    bindIfaceTyVars tvs $ \tvs' ->
+    thing_inside (tv' : tvs')
+
 bindIfaceTyVar :: IfaceTvBndr -> (TyVar -> IfL a) -> IfL a
 bindIfaceTyVar (occ,kind) thing_inside
   = do  { name <- newIfaceName (mkTyVarOccFS occ)