WIP in the direction of linting StepsProvwip/amg/T8095

The awkward part here is that we need access to the FamInstEnvs whenver
we call Lint. I've attmepted to look them up where necessary and pass
them around, but this is unlikely to be correct yet.

25 files changed, 165 insertions, 90 deletions

diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs
index fdd7da96c0..cf094619b3 100644
--- a/compiler/GHC/Core/Lint.hs
+++ b/compiler/GHC/Core/Lint.hs
@@ -34,6 +34,7 @@ import GHC.Driver.Ppr
 import GHC.Driver.Env
 
 import GHC.Core
+import GHC.Core.FamInstEnv
 import GHC.Core.FVs
 import GHC.Core.Utils
 import GHC.Core.Stats ( coreBindsStats )
@@ -83,6 +84,8 @@ import GHC.Core.Coercion.Opt ( checkAxInstCo )
 import GHC.Core.Opt.Arity    ( typeArity )
 import GHC.Types.Demand      ( splitDmdSig, isDeadEndDiv )
 import GHC.Types.TypeEnv
+import GHC.Tc.Solver.Monad ( stepsWithEvidence )
+import GHC.Unit.External
 import GHC.Unit.Module.ModGuts
 import GHC.Runtime.Context
 
@@ -283,19 +286,20 @@ be, and it makes a convenient place for them.  They print out stuff
 before and after core passes, and do Core Lint when necessary.
 -}
 
-endPass :: CoreToDo -> CoreProgram -> [CoreRule] -> CoreM ()
-endPass pass binds rules
+endPass :: CoreToDo -> CoreProgram -> [CoreRule] -> [FamInst] -> CoreM ()
+endPass pass binds rules fam_insts
   = do { hsc_env <- getHscEnv
        ; print_unqual <- getPrintUnqualified
-       ; liftIO $ endPassIO hsc_env print_unqual pass binds rules }
+       ; liftIO $ endPassIO hsc_env print_unqual pass binds rules fam_insts }
 
 endPassIO :: HscEnv -> PrintUnqualified
-          -> CoreToDo -> CoreProgram -> [CoreRule] -> IO ()
+          -> CoreToDo -> CoreProgram -> [CoreRule] -> [FamInst] -> IO ()
 -- Used by the IO-is CorePrep too
-endPassIO hsc_env print_unqual pass binds rules
+endPassIO hsc_env print_unqual pass binds rules fam_insts
   = do { dumpPassResult logger dflags print_unqual mb_flag
                         (ppr pass) (pprPassDetails pass) binds rules
-       ; lintPassResult hsc_env pass binds }
+       ; fam_envs <- getFamInstEnvsIO hsc_env fam_insts
+       ; lintPassResult hsc_env fam_envs pass binds }
   where
     logger  = hsc_logger hsc_env
     dflags  = hsc_dflags hsc_env
@@ -304,6 +308,17 @@ endPassIO hsc_env print_unqual pass binds rules
                           | dopt Opt_D_verbose_core2core dflags -> Just flag
                 _ -> Nothing
 
+-- AMG TODO: it's far from clear this is right
+getFamInstEnvsIO :: HscEnv -> [FamInst] -> IO FamInstEnvs
+getFamInstEnvsIO hsc_env this_module_fam_insts
+  = do { let (_home_insts, home_fam_inst_list) = hptInstances hsc_env (\_ -> True)
+       ; let home_fam_insts = extendFamInstEnvList emptyFamInstEnv home_fam_inst_list
+       ; let (_, ic_fam_insts) = ic_instances (hsc_IC hsc_env)
+       ; let all_home_fam_insts = extendFamInstEnvList home_fam_insts (this_module_fam_insts ++ ic_fam_insts)
+       ; eps_fam_insts <- eps_fam_inst_env <$> hscEPS hsc_env
+       ; return (eps_fam_insts, all_home_fam_insts)
+       }
+
 dumpIfSet :: Logger -> DynFlags -> Bool -> CoreToDo -> SDoc -> SDoc -> IO ()
 dumpIfSet logger dflags dump_me pass extra_info doc
   = Logger.dumpIfSet logger dflags dump_me (showSDoc dflags (ppr pass <+> extra_info)) doc
@@ -376,12 +391,12 @@ coreDumpFlag (CoreDoPasses {})        = Nothing
 ************************************************************************
 -}
 
-lintPassResult :: HscEnv -> CoreToDo -> CoreProgram -> IO ()
-lintPassResult hsc_env pass binds
+lintPassResult :: HscEnv -> FamInstEnvs -> CoreToDo -> CoreProgram -> IO ()
+lintPassResult hsc_env fam_envs pass binds
   | not (gopt Opt_DoCoreLinting dflags)
   = return ()
   | otherwise
-  = do { let warns_and_errs = lintCoreBindings dflags pass (interactiveInScope $ hsc_IC hsc_env) binds
+  = do { let warns_and_errs = lintCoreBindings dflags fam_envs pass (interactiveInScope $ hsc_IC hsc_env) binds
        ; Err.showPass logger dflags ("Core Linted result of " ++ showPpr dflags pass)
        ; displayLintResults logger dflags (showLintWarnings pass) (ppr pass)
                             (pprCoreBindings binds) warns_and_errs }
@@ -434,10 +449,12 @@ lintInteractiveExpr :: SDoc -- ^ The source of the linted expression
 lintInteractiveExpr what hsc_env expr
   | not (gopt Opt_DoCoreLinting dflags)
   = return ()
-  | Just err <- lintExpr dflags (interactiveInScope $ hsc_IC hsc_env) expr
-  = displayLintResults logger dflags False what (pprCoreExpr expr) (emptyBag, err)
   | otherwise
-  = return ()
+  = do { fam_envs <- getFamInstEnvsIO hsc_env [] -- AMG TODO: is empty list right?
+       ; case lintExpr dflags fam_envs (interactiveInScope $ hsc_IC hsc_env) expr of
+           Just err -> displayLintResults logger dflags False what (pprCoreExpr expr) (emptyBag, err)
+           Nothing   -> return ()
+       }
   where
     dflags = hsc_dflags hsc_env
     logger = hsc_logger hsc_env
@@ -469,12 +486,12 @@ interactiveInScope ictxt
               -- where t is a RuntimeUnk (see TcType)
 
 -- | Type-check a 'CoreProgram'. See Note [Core Lint guarantee].
-lintCoreBindings :: DynFlags -> CoreToDo -> [Var] -> CoreProgram -> WarnsAndErrs
+lintCoreBindings :: DynFlags -> FamInstEnvs -> CoreToDo -> [Var] -> CoreProgram -> WarnsAndErrs
 --   Returns (warnings, errors)
 -- If you edit this function, you may need to update the GHC formalism
 -- See Note [GHC Formalism]
-lintCoreBindings dflags pass local_in_scope binds
-  = initL dflags flags local_in_scope $
+lintCoreBindings dflags fam_envs pass local_in_scope binds
+  = initL dflags flags fam_envs local_in_scope $
     addLoc TopLevelBindings           $
     do { checkL (null dups) (dupVars dups)
        ; checkL (null ext_dups) (dupExtVars ext_dups)
@@ -554,17 +571,18 @@ hence the `TopLevelFlag` on `tcPragExpr` in GHC.IfaceToCore.
 
 lintUnfolding :: Bool               -- True <=> is a compulsory unfolding
               -> DynFlags
+              -> FamInstEnvs
               -> SrcLoc
               -> VarSet             -- Treat these as in scope
               -> CoreExpr
               -> Maybe (Bag SDoc) -- Nothing => OK
 
-lintUnfolding is_compulsory dflags locn var_set expr
+lintUnfolding is_compulsory dflags fam_envs locn var_set expr
   | isEmptyBag errs = Nothing
   | otherwise       = Just errs
   where
     vars = nonDetEltsUniqSet var_set
-    (_warns, errs) = initL dflags (defaultLintFlags dflags) vars $
+    (_warns, errs) = initL dflags (defaultLintFlags dflags) fam_envs vars $
                      if is_compulsory
                        -- See Note [Checking for levity polymorphism]
                      then noLPChecks linter
@@ -573,15 +591,16 @@ lintUnfolding is_compulsory dflags locn var_set expr
              lintCoreExpr expr
 
 lintExpr :: DynFlags
+         -> FamInstEnvs
          -> [Var]               -- Treat these as in scope
          -> CoreExpr
          -> Maybe (Bag SDoc)  -- Nothing => OK
 
-lintExpr dflags vars expr
+lintExpr dflags fam_envs vars expr
   | isEmptyBag errs = Nothing
   | otherwise       = Just errs
   where
-    (_warns, errs) = initL dflags (defaultLintFlags dflags) vars linter
+    (_warns, errs) = initL dflags (defaultLintFlags dflags) fam_envs vars linter
     linter = addLoc TopLevelBindings $
              lintCoreExpr expr
 
@@ -2095,7 +2114,7 @@ lintCoercion co@(UnivCo prov r ty1 ty2)
        ; ty2' <- lintType ty2
        ; let k1 = typeKind ty1'
              k2 = typeKind ty2'
-       ; prov' <- lint_prov k1 k2 prov
+       ; prov' <- lint_prov k1 ty1' k2 ty2' prov
 
        ; when (r /= Phantom && classifiesTypeWithValues k1
                             && classifiesTypeWithValues k2)
@@ -2144,22 +2163,47 @@ lintCoercion co@(UnivCo prov r ty1 ty2)
                 _          -> return ()
             }
 
-     lint_prov k1 k2 (PhantomProv kco)
+     lint_prov k1 _ k2 _ (PhantomProv kco)
        = do { kco' <- lintStarCoercion kco
             ; lintRole co Phantom r
             ; check_kinds kco' k1 k2
             ; return (PhantomProv kco') }
 
-     lint_prov k1 k2 (ProofIrrelProv kco)
+     lint_prov k1 _ k2 _ (ProofIrrelProv kco)
        = do { lintL (isCoercionTy ty1) (mkBadProofIrrelMsg ty1 co)
             ; lintL (isCoercionTy ty2) (mkBadProofIrrelMsg ty2 co)
             ; kco' <- lintStarCoercion kco
             ; check_kinds kco k1 k2
             ; return (ProofIrrelProv kco') }
 
-     lint_prov _ _ prov@(PluginProv _) = return prov
-
-     lint_prov _ _ prov@(StepsProv _ _) = return prov -- AMG TODO: actually lint this
+     lint_prov _ _ _ _ prov@(PluginProv _) = return prov
+
+     lint_prov _ ty1' _ ty2' prov@(StepsProv m n)
+       = do { fam_envs <- getFamInstEnvs
+            ; let mb1 = stepsWithEvidence m fam_envs ty1'
+            ; let mb2 = stepsWithEvidence n fam_envs ty2'
+            ; case (mb1, mb2) of
+                (Just (u, co1), Just (v, co2)) -> do { checkL (u `eqType` v) (report mb1 mb2 "inputs do not reduce to equal types")
+                                                     ; lco <- lintCoercion (mkSymCo co1 `mkTransCo` co2)
+                                                     ; checkL (coercionLKind lco `eqType` ty1')
+                                                              (report mb1 mb2 "coercion left type wrong")
+                                                     ; checkL (coercionRKind lco `eqType` ty2')
+                                                              (report mb1 mb2 "coercion right type wrong")
+                                                     ; return ()
+                                                     }
+                _ -> addWarnL (report mb1 mb2 "could not reduce")
+            ; return prov
+            }
+       where
+         report u v s =
+             hang (text $ "Invalid steps coercion: " ++ s)
+                     2 (vcat [ text "LHS:" <+> ppr ty1'
+                             , text "Expected" <+> ppr m <+> text "steps"
+                             , text "Reduced LHS:" <+> ppr u
+                             , text "RHS:" <+> ppr ty2'
+                             , text "Expected" <+> ppr n <+> text "steps"
+                             , text "Reduced RHS:" <+> ppr v
+                             ])
 
      check_kinds kco k1 k2
        = do { let Pair k1' k2' = coercionKind kco
@@ -2335,12 +2379,13 @@ lintCoercion (HoleCo h)
 
 lintAxioms :: Logger
            -> DynFlags
+           -> FamInstEnvs
            -> SDoc -- ^ The source of the linted axioms
            -> [CoAxiom Branched]
            -> IO ()
-lintAxioms logger dflags what axioms =
+lintAxioms logger dflags fam_envs what axioms =
   displayLintResults logger dflags True what (vcat $ map pprCoAxiom axioms) $
-  initL dflags (defaultLintFlags dflags) [] $
+  initL dflags (defaultLintFlags dflags) fam_envs [] $
   do { mapM_ lint_axiom axioms
      ; let axiom_groups = groupWith coAxiomTyCon axioms
      ; mapM_ lint_axiom_group axiom_groups }
@@ -2498,6 +2543,7 @@ compatible_branches (CoAxBranch { cab_tvs = tvs1
                              substTy unifying_subst rhs2'
       Nothing             -> True
 
+
 {-
 ************************************************************************
 *                                                                      *
@@ -2532,6 +2578,7 @@ data LintEnv
                                -- See Note [Join points]
 
        , le_dynflags :: DynFlags     -- DynamicFlags
+       , le_fam_envs :: FamInstEnvs
        , le_ue_aliases :: NameEnv UsageEnv -- Assigns usage environments to the
                                            -- alias-like binders, as found in
                                            -- non-recursive lets.
@@ -2697,9 +2744,9 @@ data LintLocInfo
   | InCo   Coercion     -- Inside a coercion
   | InAxiom (CoAxiom Branched)   -- Inside a CoAxiom
 
-initL :: DynFlags -> LintFlags -> [Var]
+initL :: DynFlags -> LintFlags -> FamInstEnvs -> [Var]
        -> LintM a -> WarnsAndErrs    -- Warnings and errors
-initL dflags flags vars m
+initL dflags flags fam_envs vars m
   = case unLintM m env (emptyBag, emptyBag) of
       (Just _, errs) -> errs
       (Nothing, errs@(_, e)) | not (isEmptyBag e) -> errs
@@ -2713,6 +2760,7 @@ initL dflags flags vars m
              , le_joins = emptyVarSet
              , le_loc = []
              , le_dynflags = dflags
+             , le_fam_envs = fam_envs
              , le_ue_aliases = emptyNameEnv }
 
 setReportUnsat :: Bool -> LintM a -> LintM a
@@ -2826,6 +2874,9 @@ getValidJoins = LintM (\ env errs -> (Just (le_joins env), errs))
 getTCvSubst :: LintM TCvSubst
 getTCvSubst = LintM (\ env errs -> (Just (le_subst env), errs))
 
+getFamInstEnvs :: LintM FamInstEnvs
+getFamInstEnvs = LintM (\ env errs -> (Just (le_fam_envs env), errs))
+
 getUEAliases :: LintM (NameEnv UsageEnv)
 getUEAliases = LintM (\ env errs -> (Just (le_ue_aliases env), errs))
 
diff --git a/compiler/GHC/Core/Opt/Pipeline.hs b/compiler/GHC/Core/Opt/Pipeline.hs
index f81f45eba2..07e93b8059 100644
--- a/compiler/GHC/Core/Opt/Pipeline.hs
+++ b/compiler/GHC/Core/Opt/Pipeline.hs
@@ -472,7 +472,7 @@ runCorePasses passes guts
       withTiming logger dflags (ppr pass <+> brackets (ppr mod))
                    (const ()) $ do
             guts' <- lintAnnots (ppr pass) (doCorePass pass) guts
-            endPass pass (mg_binds guts') (mg_rules guts')
+            endPass pass (mg_binds guts') (mg_rules guts') (mg_fam_insts guts')
             return guts'
 
     mod = mg_module guts
@@ -817,7 +817,7 @@ simplifyPgmIO pass@(CoreDoSimplify max_iterations mode)
 
                 -- Dump the result of this iteration
            dump_end_iteration logger dflags print_unqual iteration_no counts1 binds2 rules1 ;
-           lintPassResult hsc_env pass binds2 ;
+           lintPassResult hsc_env fam_envs pass binds2 ;
 
                 -- Loop
            do_iteration (iteration_no + 1) (counts1:counts_so_far) binds2 rules1
diff --git a/compiler/GHC/CoreToStg/Prep.hs b/compiler/GHC/CoreToStg/Prep.hs
index 74616683e3..6faea372f9 100644
--- a/compiler/GHC/CoreToStg/Prep.hs
+++ b/compiler/GHC/CoreToStg/Prep.hs
@@ -37,6 +37,7 @@ import GHC.Builtin.Types
 import GHC.Builtin.Types.Prim ( realWorldStatePrimTy )
 import GHC.Types.Id.Make ( realWorldPrimId, mkPrimOpId )
 
+import GHC.Core.FamInstEnv
 import GHC.Core.Utils
 import GHC.Core.Opt.Arity
 import GHC.Core.FVs
@@ -187,9 +188,9 @@ type CpeRhs  = CoreExpr    -- Non-terminal 'rhs'
 ************************************************************************
 -}
 
-corePrepPgm :: HscEnv -> Module -> ModLocation -> CoreProgram -> [TyCon]
+corePrepPgm :: HscEnv -> Module -> ModLocation -> CoreProgram -> [TyCon] -> [FamInst]
             -> IO (CoreProgram, S.Set CostCentre)
-corePrepPgm hsc_env this_mod mod_loc binds data_tycons =
+corePrepPgm hsc_env this_mod mod_loc binds data_tycons fam_insts =
     withTiming logger dflags
                (text "CorePrep"<+>brackets (ppr this_mod))
                (\(a,b) -> a `seqList` b `seq` ()) $ do
@@ -211,7 +212,7 @@ corePrepPgm hsc_env this_mod mod_loc binds data_tycons =
                       floats2 <- corePrepTopBinds initialCorePrepEnv implicit_binds
                       return (deFloatTop (floats1 `appendFloats` floats2))
 
-    endPassIO hsc_env alwaysQualify CorePrep binds_out []
+    endPassIO hsc_env alwaysQualify CorePrep binds_out [] fam_insts
     return (binds_out, cost_centres)
   where
     dflags = hsc_dflags hsc_env
diff --git a/compiler/GHC/Driver/Main.hs b/compiler/GHC/Driver/Main.hs
index 296a855acf..dc6eb4766a 100644
--- a/compiler/GHC/Driver/Main.hs
+++ b/compiler/GHC/Driver/Main.hs
@@ -1555,10 +1555,10 @@ hscSimpleIface' tc_result mb_old_iface = do
 --------------------------------------------------------------
 
 -- | Compile to hard-code.
-hscGenHardCode :: HscEnv -> CgGuts -> ModLocation -> FilePath
+hscGenHardCode :: HscEnv -> CgGuts -> ModLocation -> FilePath -> [FamInst]
                -> IO (FilePath, Maybe FilePath, [(ForeignSrcLang, FilePath)], CgInfos)
                -- ^ @Just f@ <=> _stub.c is f
-hscGenHardCode hsc_env cgguts location output_filename = do
+hscGenHardCode hsc_env cgguts location output_filename fam_insts = do
         let CgGuts{ -- This is the last use of the ModGuts in a compilation.
                     -- From now on, we just use the bits we need.
                     cg_module   = this_mod,
@@ -1581,7 +1581,7 @@ hscGenHardCode hsc_env cgguts location output_filename = do
         -- Do saturation and convert to A-normal form
         (prepd_binds, local_ccs) <- {-# SCC "CorePrep" #-}
                        corePrepPgm hsc_env this_mod location
-                                   core_binds data_tycons
+                                   core_binds data_tycons fam_insts
 
         -----------------  Convert to STG ------------------
         (stg_binds, denv, (caf_ccs, caf_cc_stacks))
@@ -1637,8 +1637,9 @@ hscGenHardCode hsc_env cgguts location output_filename = do
 hscInteractive :: HscEnv
                -> CgGuts
                -> ModLocation
+               -> [FamInst]
                -> IO (Maybe FilePath, CompiledByteCode, [SptEntry])
-hscInteractive hsc_env cgguts location = do
+hscInteractive hsc_env cgguts location fam_insts = do
     let dflags = hsc_dflags hsc_env
     let logger = hsc_logger hsc_env
     let tmpfs  = hsc_tmpfs hsc_env
@@ -1659,7 +1660,7 @@ hscInteractive hsc_env cgguts location = do
     -- PREPARE FOR CODE GENERATION
     -- Do saturation and convert to A-normal form
     (prepd_binds, _) <- {-# SCC "CorePrep" #-}
-                   corePrepPgm hsc_env this_mod location core_binds data_tycons
+                   corePrepPgm hsc_env this_mod location core_binds data_tycons fam_insts
 
     (stg_binds, _infotable_prov, _caf_ccs__caf_cc_stacks)
       <- {-# SCC "CoreToStg" #-}
@@ -1974,7 +1975,7 @@ hscParsedDecls hsc_env decls = runInteractiveHsc hsc_env $ do
     {- Prepare For Code Generation -}
     -- Do saturation and convert to A-normal form
     (prepd_binds, _) <- {-# SCC "CorePrep" #-}
-      liftIO $ corePrepPgm hsc_env this_mod iNTERACTIVELoc core_binds data_tycons
+      liftIO $ corePrepPgm hsc_env this_mod iNTERACTIVELoc core_binds data_tycons fam_insts
 
     (stg_binds, _infotable_prov, _caf_ccs__caf_cc_stacks)
         <- {-# SCC "CoreToStg" #-}
diff --git a/compiler/GHC/Driver/Pipeline.hs b/compiler/GHC/Driver/Pipeline.hs
index e6b7be62ef..eed38225ff 100644
--- a/compiler/GHC/Driver/Pipeline.hs
+++ b/compiler/GHC/Driver/Pipeline.hs
@@ -98,6 +98,7 @@ import GHC.Unit
 import GHC.Unit.Env
 import GHC.Unit.State
 import GHC.Unit.Finder
+import GHC.Unit.Module.ModDetails
 import GHC.Unit.Module.ModSummary
 import GHC.Unit.Module.ModIface
 import GHC.Unit.Module.Graph (needsTemplateHaskellOrQQ)
@@ -267,7 +268,7 @@ compileOne' m_tc_result mHscMessage
             hmi_details <- liftIO $ initModDetails hsc_env' summary final_iface
             liftIO $ hscMaybeWriteIface logger dflags True final_iface mb_old_iface_hash (ms_location summary)
 
-            (hasStub, comp_bc, spt_entries) <- hscInteractive hsc_env' cgguts mod_location
+            (hasStub, comp_bc, spt_entries) <- hscInteractive hsc_env' cgguts mod_location (md_fam_insts hmi_details)
 
             stub_o <- case hasStub of
                       Nothing -> return []
@@ -1384,7 +1385,7 @@ runPhase (HscOut src_flavour mod_name result) _ = do
                     PipeState{hsc_env=hsc_env'} <- getPipeState
 
                     (outputFilename, mStub, foreign_files, cg_infos) <- liftIO $
-                      hscGenHardCode hsc_env' cgguts mod_location output_fn
+                      hscGenHardCode hsc_env' cgguts mod_location output_fn [] {-(md_fam_insts mod_details)-} -- TODO
 
                     let dflags = hsc_dflags hsc_env'
                     final_iface <- liftIO (mkFullIface hsc_env' partial_iface (Just cg_infos))
diff --git a/compiler/GHC/HsToCore.hs b/compiler/GHC/HsToCore.hs
index a4bbc290e2..e1f4807a20 100644
--- a/compiler/GHC/HsToCore.hs
+++ b/compiler/GHC/HsToCore.hs
@@ -184,7 +184,7 @@ deSugar hsc_env
         -- You might think it doesn't matter, but the simplifier brings all top-level
         -- things into the in-scope set before simplifying; so we get no unfolding for F#!
 
-        ; endPassIO hsc_env print_unqual CoreDesugar final_pgm rules_for_imps
+        ; endPassIO hsc_env print_unqual CoreDesugar final_pgm rules_for_imps fam_insts
         ; let simpl_opts = initSimpleOpts dflags
         ; let (ds_binds, ds_rules_for_imps, occ_anald_binds)
                 = simpleOptPgm simpl_opts mod final_pgm rules_for_imps
@@ -193,7 +193,7 @@ deSugar hsc_env
         ; dumpIfSet_dyn logger dflags Opt_D_dump_occur_anal "Occurrence analysis"
             FormatCore (pprCoreBindings occ_anald_binds $$ pprRules ds_rules_for_imps )
 
-        ; endPassIO hsc_env print_unqual CoreDesugarOpt ds_binds ds_rules_for_imps
+        ; endPassIO hsc_env print_unqual CoreDesugarOpt ds_binds ds_rules_for_imps fam_insts
 
         ; let used_names = mkUsedNames tcg_env
               pluginModules = map lpModule (hsc_plugins hsc_env)
diff --git a/compiler/GHC/HsToCore/Monad.hs b/compiler/GHC/HsToCore/Monad.hs
index a16f70cded..38d45b48b3 100644
--- a/compiler/GHC/HsToCore/Monad.hs
+++ b/compiler/GHC/HsToCore/Monad.hs
@@ -318,7 +318,8 @@ mkDsEnvs :: UnitEnv -> Module -> GlobalRdrEnv -> TypeEnv -> FamInstEnv
 mkDsEnvs unit_env mod rdr_env type_env fam_inst_env msg_var cc_st_var
          complete_matches
   = let if_genv = IfGblEnv { if_doc       = text "mkDsEnvs",
-                             if_rec_types = Just (mod, return type_env) }
+                             if_rec_types = Just (mod, return type_env)
+                           , if_fam_insts = Just (mempty, fam_inst_env) } -- AMY TODO: EPS fam insts? how come DS doesn't need them?
         if_lenv = mkIfLclEnv mod (text "GHC error in desugarer lookup in" <+> ppr mod)
                              NotBoot
         real_span = realSrcLocSpan (mkRealSrcLoc (moduleNameFS (moduleName mod)) 1 1)
diff --git a/compiler/GHC/Iface/Tidy.hs b/compiler/GHC/Iface/Tidy.hs
index c6175b2602..6abe996127 100644
--- a/compiler/GHC/Iface/Tidy.hs
+++ b/compiler/GHC/Iface/Tidy.hs
@@ -436,7 +436,7 @@ tidyProgram hsc_env  (ModGuts { mg_module           = mod
               ; alg_tycons = filter isAlgTyCon tcs
               }
 
-        ; endPassIO hsc_env print_unqual CoreTidy all_tidy_binds tidy_rules
+        ; endPassIO hsc_env print_unqual CoreTidy all_tidy_binds tidy_rules fam_insts
 
           -- If the endPass didn't print the rules, but ddump-rules is
           -- on, print now
diff --git a/compiler/GHC/IfaceToCore.hs b/compiler/GHC/IfaceToCore.hs
index 24a72fe39d..5b305945b9 100644
--- a/compiler/GHC/IfaceToCore.hs
+++ b/compiler/GHC/IfaceToCore.hs
@@ -1211,13 +1211,16 @@ tcIfaceRule (IfaceRule {ifRuleName = name, ifActivation = act, ifRuleBndrs = bnd
                    ; rhs'   <- tcIfaceExpr rhs
                    ; whenGOptM Opt_DoCoreLinting $ do
                       { dflags <- getDynFlags
-                      ; (_, lcl_env) <- getEnvs
+                      ; (gbl_env, lcl_env) <- getEnvs
                       ; let in_scope :: [Var]
                             in_scope = ((nonDetEltsUFM $ if_tv_env lcl_env) ++
                                         (nonDetEltsUFM $ if_id_env lcl_env) ++
                                         bndrs' ++
                                         exprsFreeIdsList args')
-                      ; case lintExpr dflags in_scope rhs' of
+                      ; let fam_envs = case if_fam_insts gbl_env of -- AMG TODO: clean up
+                                         Just xs -> xs
+                                         Nothing -> panic "tcIfaceRule: missing if_fam_insts"
+                      ; case lintExpr dflags fam_envs in_scope rhs' of
                           Nothing   -> return ()
                           Just errs -> do
                             logger <- getLogger
@@ -1747,7 +1750,8 @@ tcPragExpr is_compulsory toplvl name expr
         in_scope <- get_in_scope
         dflags   <- getDynFlags
         logger   <- getLogger
-        case lintUnfolding is_compulsory dflags noSrcLoc in_scope core_expr' of
+        fam_envs <- fromJust . if_fam_insts <$> getGblEnv -- AMG TODO
+        case lintUnfolding is_compulsory dflags fam_envs noSrcLoc in_scope core_expr' of
           Nothing   -> return ()
           Just errs -> liftIO $
             displayLintResults logger dflags False doc
diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs
index 4f4f53f1cf..a5ce1c1ff2 100644
--- a/compiler/GHC/Tc/Gen/App.hs
+++ b/compiler/GHC/Tc/Gen/App.hs
@@ -27,7 +27,7 @@ import GHC.Hs
 import GHC.Tc.Utils.Monad
 import GHC.Tc.Utils.Unify
 import GHC.Tc.Utils.Instantiate
-import GHC.Tc.Instance.Family ( tcGetFamInstEnvs, tcLookupDataFamInst_maybe )
+import GHC.Tc.Instance.Family ( tcLookupDataFamInst_maybe )
 import GHC.Tc.Gen.HsType
 import GHC.Tc.Utils.TcMType
 import GHC.Tc.Types.Origin
diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs
index 386f1959b6..23fd624db8 100644
--- a/compiler/GHC/Tc/Gen/Bind.hs
+++ b/compiler/GHC/Tc/Gen/Bind.hs
@@ -45,7 +45,6 @@ import GHC.Tc.Gen.Pat
 import GHC.Tc.Utils.TcMType
 import GHC.Core.Multiplicity
 import GHC.Core.FamInstEnv( normaliseType )
-import GHC.Tc.Instance.Family( tcGetFamInstEnvs )
 import GHC.Tc.Utils.TcType
 import GHC.Core.Type (mkStrLitTy, tidyOpenType, mkCastTy)
 import GHC.Builtin.Types ( mkBoxedTupleTy )
diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs
index ecd07c6059..3404563b6f 100644
--- a/compiler/GHC/Tc/Gen/Expr.hs
+++ b/compiler/GHC/Tc/Gen/Expr.hs
@@ -44,7 +44,6 @@ import GHC.Tc.Utils.Instantiate
 import GHC.Tc.Gen.App
 import GHC.Tc.Gen.Head
 import GHC.Tc.Gen.Bind        ( tcLocalBinds )
-import GHC.Tc.Instance.Family ( tcGetFamInstEnvs )
 import GHC.Core.FamInstEnv    ( FamInstEnvs )
 import GHC.Rename.Env         ( addUsedGRE )
 import GHC.Tc.Utils.Env
diff --git a/compiler/GHC/Tc/Gen/Head.hs b/compiler/GHC/Tc/Gen/Head.hs
index feb984fc26..5b1c3bdb25 100644
--- a/compiler/GHC/Tc/Gen/Head.hs
+++ b/compiler/GHC/Tc/Gen/Head.hs
@@ -41,7 +41,7 @@ import GHC.Tc.Utils.Monad
 import GHC.Tc.Utils.Unify
 import GHC.Types.Basic
 import GHC.Tc.Utils.Instantiate
-import GHC.Tc.Instance.Family ( tcGetFamInstEnvs, tcLookupDataFamInst )
+import GHC.Tc.Instance.Family ( tcLookupDataFamInst )
 import GHC.Core.FamInstEnv    ( FamInstEnvs )
 import GHC.Core.UsageEnv      ( unitUE )
 import GHC.Rename.Env         ( addUsedGRE )
diff --git a/compiler/GHC/Tc/Gen/Splice.hs b/compiler/GHC/Tc/Gen/Splice.hs
index 589513af97..eff0f6bf14 100644
--- a/compiler/GHC/Tc/Gen/Splice.hs
+++ b/compiler/GHC/Tc/Gen/Splice.hs
@@ -53,7 +53,6 @@ import GHC.Tc.Utils.Zonk
 import GHC.Tc.Solver
 import GHC.Tc.Utils.TcMType
 import GHC.Tc.Gen.HsType
-import GHC.Tc.Instance.Family
 import GHC.Tc.Utils.Instantiate
 
 import GHC.Core.Multiplicity
diff --git a/compiler/GHC/Tc/Instance/Class.hs b/compiler/GHC/Tc/Instance/Class.hs
index 84b523eb93..83417be42e 100644
--- a/compiler/GHC/Tc/Instance/Class.hs
+++ b/compiler/GHC/Tc/Instance/Class.hs
@@ -23,7 +23,7 @@ import GHC.Tc.Utils.Instantiate(instDFunType, tcInstType)
 import GHC.Tc.Instance.Typeable
 import GHC.Tc.Utils.TcMType
 import GHC.Tc.Types.Evidence
-import GHC.Tc.Instance.Family( tcGetFamInstEnvs, tcInstNewTyCon_maybe, tcLookupDataFamInst )
+import GHC.Tc.Instance.Family( tcInstNewTyCon_maybe, tcLookupDataFamInst )
 import GHC.Rename.Env( addUsedGRE )
 
 import GHC.Builtin.Types
diff --git a/compiler/GHC/Tc/Instance/Family.hs b/compiler/GHC/Tc/Instance/Family.hs
index 65e91608b9..d70b3ec381 100644
--- a/compiler/GHC/Tc/Instance/Family.hs
+++ b/compiler/GHC/Tc/Instance/Family.hs
@@ -1034,10 +1034,3 @@ reportConflictInstErr fam_inst (match1 : _)
    -- The sortBy just arranges that instances are displayed in order
    -- of source location, which reduced wobbling in error messages,
    -- and is better for users
-
-tcGetFamInstEnvs :: TcM FamInstEnvs
--- Gets both the external-package inst-env
--- and the home-pkg inst env (includes module being compiled)
-tcGetFamInstEnvs
-  = do { eps <- getEps; env <- getGblEnv
-       ; return (eps_fam_inst_env eps, tcg_fam_inst_env env) }
diff --git a/compiler/GHC/Tc/Module.hs b/compiler/GHC/Tc/Module.hs
index 777086343b..3877f21498 100644
--- a/compiler/GHC/Tc/Module.hs
+++ b/compiler/GHC/Tc/Module.hs
@@ -115,6 +115,7 @@ import GHC.Core.DataCon
 import GHC.Core.Type
 import GHC.Core.Class
 import GHC.Core.Coercion.Axiom
+import GHC.Core.Lint
 import GHC.Core.Unify( RoughMatchTc(..) )
 import GHC.Core.FamInstEnv
    ( FamInst, pprFamInst, famInstsRepTyCons
@@ -3149,3 +3150,19 @@ mark_plugin_unsafe dflags = unless (gopt Opt_PluginTrustworthy dflags) $
     unsafeText = "Use of plugins makes the module unsafe"
     pluginUnsafe = unitBag ( mkPlainMsgEnvelope dflags WarningWithoutFlag noSrcSpan
                                    (Outputable.text unsafeText) )
+
+{- *********************************************************************
+*                                                                      *
+                  Linting a TcGblEnv
+*                                                                      *
+********************************************************************* -}
+
+-- | Check the 'TcGblEnv' for consistency. Currently, only checks
+-- axioms, but should check other aspects, too.
+lintGblEnv :: Logger -> DynFlags -> TcGblEnv -> TcM ()
+lintGblEnv logger dflags tcg_env
+  = do { fam_envs <- tcGetFamInstEnvs
+       ; liftIO $ lintAxioms logger dflags fam_envs (text "TcGblEnv axioms") axioms
+       }
+  where
+    axioms = typeEnvCoAxioms (tcg_type_env tcg_env)
diff --git a/compiler/GHC/Tc/Plugin.hs b/compiler/GHC/Tc/Plugin.hs
index b4d4fc5ad2..2e441d5ca9 100644
--- a/compiler/GHC/Tc/Plugin.hs
+++ b/compiler/GHC/Tc/Plugin.hs
@@ -56,7 +56,6 @@ import qualified GHC.Tc.Utils.Monad     as TcM
 import qualified GHC.Tc.Solver.Monad    as TcS
 import qualified GHC.Tc.Utils.Env       as TcM
 import qualified GHC.Tc.Utils.TcMType   as TcM
-import qualified GHC.Tc.Instance.Family as TcM
 import qualified GHC.Iface.Env          as IfaceEnv
 import qualified GHC.Unit.Finder        as Finder
 
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index 45b564f99d..6cc7cc5dda 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -122,7 +122,7 @@ module GHC.Tc.Solver.Monad (
 
     -- Misc
     getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
-    matchFam, matchFamTcM, stepFam,
+    matchFam, matchFamTcM, stepFam, steps, stepsWithEvidence,
     checkWellStagedDFun,
     pprEq,                                   -- Smaller utils, re-exported from TcM
                                              -- TODO (DV): these are only really used in the
@@ -4058,6 +4058,20 @@ isSteps_maybe (Rep.UnivCo (Rep.StepsProv m n) _ _ _) = Just (Pair m n)
 isSteps_maybe _ = Nothing
 
 
+stepsWithEvidence :: Int -> FamInstEnvs -> Type -> Maybe (Type, Coercion)
+-- ^ Given a type, perform the given number of steps and produce a coercion.
+stepsWithEvidence n fam_envs ty = go n (ty, mkNomReflCo ty)
+  where
+    go :: Int -> (Type, Coercion) -> Maybe (Type, Coercion)
+    go !i (ty,prev_co)
+      | i <= 0 = Just (ty,prev_co)
+      | Just ty' <- tcView ty = go i (ty',prev_co)
+      | Rep.TyConApp tycon args <- ty
+      , Just (co, ty') <- reduceTyFamApp_maybe fam_envs Nominal tycon args
+                  = go (i-1) (ty', mkSymCo co `mkTransCo` prev_co)
+      | otherwise = Nothing
+
+
 {-
 Note [Residual implications]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index 076c0c0ee0..7c26cfdcb7 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/compiler/GHC/Tc/TyCl.hs
@@ -51,7 +51,6 @@ import GHC.Tc.Gen.HsType
 import GHC.Tc.Instance.Class( AssocInstInfo(..) )
 import GHC.Tc.Utils.TcMType
 import GHC.Tc.Utils.TcType
-import GHC.Tc.Instance.Family
 import GHC.Tc.Types.Origin
 
 import GHC.Builtin.Types (oneDataConTy,  unitTy, makeRecoveryTyCon )
diff --git a/compiler/GHC/Tc/Types.hs b/compiler/GHC/Tc/Types.hs
index 94d454055e..689bb8e234 100644
--- a/compiler/GHC/Tc/Types.hs
+++ b/compiler/GHC/Tc/Types.hs
@@ -79,9 +79,6 @@ module GHC.Tc.Types(
         -- Role annotations
         RoleAnnotEnv, emptyRoleAnnotEnv, mkRoleAnnotEnv,
         lookupRoleAnnot, getRoleAnnots,
-
-        -- Linting
-        lintGblEnv
   ) where
 
 #include "HsVersions.h"
@@ -104,7 +101,6 @@ import {-# SOURCE #-} GHC.Tc.Errors.Hole.FitTypes ( HoleFitPlugin )
 import GHC.Core.Type
 import GHC.Core.TyCon  ( TyCon, tyConKind )
 import GHC.Core.PatSyn ( PatSyn )
-import GHC.Core.Lint   ( lintAxioms )
 import GHC.Core.UsageEnv
 import GHC.Core.InstEnv
 import GHC.Core.FamInstEnv
@@ -275,6 +271,7 @@ data IfGblEnv
                 -- Allows a read effect, so it can be in a mutable
                 -- variable; c.f. handling the external package type env
                 -- Nothing => interactive stuff, no loops possible
+      , if_fam_insts :: Maybe FamInstEnvs
     }
 
 data IfLclEnv
@@ -1730,19 +1727,6 @@ getRoleAnnots :: [Name] -> RoleAnnotEnv -> [LRoleAnnotDecl GhcRn]
 getRoleAnnots bndrs role_env
   = mapMaybe (lookupRoleAnnot role_env) bndrs
 
-{- *********************************************************************
-*                                                                      *
-                  Linting a TcGblEnv
-*                                                                      *
-********************************************************************* -}
-
--- | Check the 'TcGblEnv' for consistency. Currently, only checks
--- axioms, but should check other aspects, too.
-lintGblEnv :: Logger -> DynFlags -> TcGblEnv -> TcM ()
-lintGblEnv logger dflags tcg_env =
-  liftIO $ lintAxioms logger dflags (text "TcGblEnv axioms") axioms
-  where
-    axioms = typeEnvCoAxioms (tcg_type_env tcg_env)
 
 -- | This is a mirror of Template Haskell's DocLoc, but the TH names are
 -- resolved to GHC names.
diff --git a/compiler/GHC/Tc/Utils/Monad.hs b/compiler/GHC/Tc/Utils/Monad.hs
index fb613c8f8d..ca41f7add8 100644
--- a/compiler/GHC/Tc/Utils/Monad.hs
+++ b/compiler/GHC/Tc/Utils/Monad.hs
@@ -143,6 +143,8 @@ module GHC.Tc.Utils.Monad(
   -- * Stuff for cost centres.
   getCCIndexM, getCCIndexTcM,
 
+  tcGetFamInstEnvs,
+
   -- * Types etc.
   module GHC.Tc.Types,
   module GHC.Data.IOEnv
@@ -2046,12 +2048,14 @@ initIfaceTcRn thing_inside
               -- When we are instantiating a signature, we DEFINITELY
               -- do not want to knot tie.
               is_instantiate = isHomeUnitInstantiating home_unit
+        ; fam_insts <- tcGetFamInstEnvs
         ; let { if_env = IfGblEnv {
                             if_doc = text "initIfaceTcRn",
                             if_rec_types =
                                 if is_instantiate
                                     then Nothing
-                                    else Just (mod, get_type_env)
+                                    else Just (mod, get_type_env),
+                        if_fam_insts = Just fam_insts
                          }
               ; get_type_env = readTcRef (tcg_type_env_var tcg_env) }
         ; setEnvs (if_env, ()) thing_inside }
@@ -2064,7 +2068,8 @@ initIfaceLoad :: HscEnv -> IfG a -> IO a
 initIfaceLoad hsc_env do_this
  = do let gbl_env = IfGblEnv {
                         if_doc = text "initIfaceLoad",
-                        if_rec_types = Nothing
+                        if_rec_types = Nothing,
+                        if_fam_insts = Nothing
                     }
       initTcRnIf 'i' hsc_env gbl_env () do_this
 
@@ -2077,7 +2082,8 @@ initIfaceCheck doc hsc_env do_this
                          Nothing        -> Nothing
           gbl_env = IfGblEnv {
                         if_doc = text "initIfaceCheck" <+> doc,
-                        if_rec_types = rec_types
+                        if_rec_types = rec_types,
+                        if_fam_insts = Nothing
                     }
       initTcRnIf 'i' hsc_env gbl_env () do_this
 
@@ -2191,3 +2197,12 @@ getCCIndexM get_ccs nm = do
 -- | See 'getCCIndexM'.
 getCCIndexTcM :: FastString -> TcM CostCentreIndex
 getCCIndexTcM = getCCIndexM tcg_cc_st
+
+
+
+tcGetFamInstEnvs :: TcM FamInstEnvs
+-- Gets both the external-package inst-env
+-- and the home-pkg inst env (includes module being compiled)
+tcGetFamInstEnvs
+  = do { eps <- getEps; env <- getGblEnv
+       ; return (eps_fam_inst_env eps, tcg_fam_inst_env env) }
diff --git a/testsuite/tests/callarity/unittest/CallArity1.hs b/testsuite/tests/callarity/unittest/CallArity1.hs
index 64800dd243..0a1516879b 100644
--- a/testsuite/tests/callarity/unittest/CallArity1.hs
+++ b/testsuite/tests/callarity/unittest/CallArity1.hs
@@ -172,7 +172,7 @@ main = do
         dflags <- getSessionDynFlags
         logger <- getLogger
         liftIO $ forM_ exprs $ \(n,e) -> do
-            case lintExpr dflags [f,scrutf,scruta] e of
+            case lintExpr dflags mempty [f,scrutf,scruta] e of
                 Just errs -> putMsg logger dflags (pprMessageBag errs $$ text "in" <+> text n)
                 Nothing -> return ()
             putMsg logger dflags (text n Outputable.<> char ':')
diff --git a/testsuite/tests/parser/should_run/CountAstDeps.stdout b/testsuite/tests/parser/should_run/CountAstDeps.stdout
index a9479a9d8d..d627cb0473 100644
--- a/testsuite/tests/parser/should_run/CountAstDeps.stdout
+++ b/testsuite/tests/parser/should_run/CountAstDeps.stdout
@@ -1,4 +1,4 @@
-Found 245 Language.Haskell.Syntax module dependencies
+Found 244 Language.Haskell.Syntax module dependencies
 GHC.Builtin.Names
 GHC.Builtin.PrimOps
 GHC.Builtin.Types
@@ -29,7 +29,6 @@ GHC.Core.DataCon
 GHC.Core.FVs
 GHC.Core.FamInstEnv
 GHC.Core.InstEnv
-GHC.Core.Lint
 GHC.Core.Make
 GHC.Core.Map.Type
 GHC.Core.Multiplicity
diff --git a/testsuite/tests/parser/should_run/CountParserDeps.stdout b/testsuite/tests/parser/should_run/CountParserDeps.stdout
index 73a238fd09..a9913e112b 100644
--- a/testsuite/tests/parser/should_run/CountParserDeps.stdout
+++ b/testsuite/tests/parser/should_run/CountParserDeps.stdout
@@ -1,4 +1,4 @@
-Found 253 GHC.Parser module dependencies
+Found 252 GHC.Parser module dependencies
 GHC.Builtin.Names
 GHC.Builtin.PrimOps
 GHC.Builtin.Types
@@ -29,7 +29,6 @@ GHC.Core.DataCon
 GHC.Core.FVs
 GHC.Core.FamInstEnv
 GHC.Core.InstEnv
-GHC.Core.Lint
 GHC.Core.Make
 GHC.Core.Map.Type
 GHC.Core.Multiplicity