More progress in tcFamTyPats

In particular, revert to taking account of the class
instance types in tcFamTyPats, but by unification rather
than by messing with tcInferApps

4 files changed, 93 insertions, 72 deletions

diff --git a/compiler/typecheck/Inst.hs b/compiler/typecheck/Inst.hs
index 4f380d37a8..fa42a0778c 100644
--- a/compiler/typecheck/Inst.hs
+++ b/compiler/typecheck/Inst.hs
@@ -484,17 +484,28 @@ no longer cut it, but it seems fine for now.
 -}
 
 ---------------------------
--- | This is used to instantiate binders when type-checking *types* only.
--- The @VarEnv Kind@ gives some known instantiations.
+-- | Instantantiate the TyConBinders of a forall type,
+--   given its decomposed form (tvs, ty)
+tcInstTyBinders :: HasDebugCallStack
+              => ([TyCoBinder], TcKind)   -- ^ The type (forall bs. ty)
+              -> TcM ([TcType], TcKind)   -- ^ Instantiated bs, substituted ty
+-- Takes a pair because that is what splitPiTysInvisible returns
 -- See also Note [Bidirectional type checking]
-tcInstTyBinders :: TCvSubst -> Maybe (VarEnv Kind)
-                -> [TyBinder] -> TcM (TCvSubst, [TcType])
-tcInstTyBinders subst mb_kind_info bndrs
-  = do { (subst, args) <- mapAccumLM (tcInstTyBinder mb_kind_info) subst bndrs
-       ; traceTc "instantiating tybinders:"
-           (vcat $ zipWith (\bndr arg -> ppr bndr <+> text ":=" <+> ppr arg)
-                           bndrs args)
-       ; return (subst, args) }
+tcInstTyBinders (bndrs, ty)
+  | null bndrs        -- It's fine for bndrs to be empty e.g. 
+  = return ([], ty)   -- Check that (Maybe :: forall {k}. k->*),
+                      --       and see the call to instTyBinders in checkExpectedKind
+                      -- A user bug to be reported as such; it is not a compiler crash!
+
+  | otherwise
+  = do { (subst, args) <- mapAccumLM (tcInstTyBinder Nothing) empty_subst bndrs
+       ; ty' <- zonkTcType (substTy subst ty)
+                   -- Why zonk the result? So that tcTyVar can
+                   -- obey (IT6) of Note [The tcType invariant]
+                   -- ToDo: SLPJ: I don't think this is needed
+       ; return (args, ty') }
+  where
+     empty_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ty))
 
 -- | Used only in *types*
 tcInstTyBinder :: Maybe (VarEnv Kind)
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 8a8c3d3b33..be04103689 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -47,7 +47,6 @@ module TcHsType (
         typeLevelMode, kindLevelMode,
 
         kindGeneralize, checkExpectedKindX,
-        instantiateTyN,
         reportFloatingKvs,
 
         -- Sort-checking kinds
@@ -867,7 +866,7 @@ bigConstraintTuple arity
 -- | Apply a type of a given kind to a list of arguments. This instantiates
 -- invisible parameters as necessary. Always consumes all the arguments,
 -- using matchExpectedFunKind as necessary.
--- This takes an optional @VarEnv Kind@ which maps kind variables to kinds.
+-- This takes an optional @VarEnv Kind@ which maps kind variables to kinds.-
 -- These kinds should be used to instantiate invisible kind variables;
 -- they come from an enclosing class for an associated type/data family.
 tcInferApps :: TcTyMode
@@ -997,10 +996,10 @@ checkExpectedKindX pp_hs_ty ty act_kind exp_kind
         -- foralls out front. If the actual kind has more, instantiate accordingly.
         -- Otherwise, just pass the type & kind through: the errors are caught
         -- in unifyType.
-        let (exp_bndrs, _)            = splitPiTysInvisible exp_kind
-            (act_bndrs, act_inner_ki) = splitPiTysInvisible act_kind
-            n_to_inst                 = length act_bndrs - length exp_bndrs
-      ; (new_args, act_kind') <- instantiateTyN n_to_inst act_bndrs act_inner_ki
+        let n_exp_invis_bndrs = invisibleTyBndrCount exp_kind
+            n_act_invis_bndrs = invisibleTyBndrCount act_kind
+            n_to_inst         = n_act_invis_bndrs - n_exp_invis_bndrs
+      ; (new_args, act_kind') <- tcInstTyBinders (splitPiTysInvisibleN n_to_inst act_kind)
 
       ; let origin = TypeEqOrigin { uo_actual   = act_kind'
                                   , uo_expected = exp_kind
@@ -1024,37 +1023,6 @@ checkExpectedKindX pp_hs_ty ty act_kind exp_kind
                       -- See Note [The tcType invariant]
                 ; return result_ty } }
 
--- | Instantiate @n@ invisible arguments to a type. If @n <= 0@, no instantiation
--- occurs. If @n@ is too big, then all available invisible arguments are instantiated.
--- (In other words, this function is very forgiving about bad values of @n@.)
--- Why zonk the result? So that tcTyVar can obey (IT6) of Note [The tcType invariant]
-instantiateTyN :: HasDebugCallStack
-               => Int                              -- ^ @n@
-               -> [TyBinder] -> TcKind             -- ^ its kind (zonked)
-               -> TcM ([TcType], TcKind)   -- ^ The inst'ed type, new args, kind (zonked)
-instantiateTyN n bndrs inner_ki
-  | n <= 0            -- It's fine for it to be < 0.  E.g.
-  = return ([], ki)   -- Check that (Maybe :: forall {k}. k->*),
-                      --       and see the call to instantiateTyN in checkExpectedKind
-                      -- A user bug to be reported as such; it is not a compiler crash!
-
-  | otherwise
-  = do { (subst, inst_args) <- tcInstTyBinders empty_subst Nothing inst_bndrs
-       ; let rebuilt_ki = mkPiTys leftover_bndrs inner_ki
-       ; ki' <- zonkTcType (substTy subst rebuilt_ki)
-       ; traceTc "instantiateTyN" (vcat [ ppr ki
-                                        , ppr n
-                                        , ppr subst
-                                        , ppr rebuilt_ki
-                                        , ppr ki' ])
-       ; return (inst_args, ki') }
-  where
-     -- NB: splitAt is forgiving with invalid numbers
-     (inst_bndrs, leftover_bndrs) = splitAt n bndrs
-     ki          = mkPiTys bndrs inner_ki
-     empty_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ki))
-
-
 ---------------------------
 tcHsMbContext :: Maybe (LHsContext GhcRn) -> TcM [PredType]
 tcHsMbContext Nothing    = return []
@@ -1141,11 +1109,13 @@ tcTyVar mode name         -- Could be a tyvar, a tycon, or a datacon
               -- the mkNakedCastTy ensures (IT5) of Note [The tcType invariant]
 
       | otherwise
-      = do { tc_kind <- zonkTcType (tyConKind tc)
-           ; let (tc_kind_bndrs, tc_inner_ki) = splitPiTysInvisible tc_kind
-           ; (tc_args, kind) <- instantiateTyN (length (tyConBinders tc))
-                                               tc_kind_bndrs tc_inner_ki
-           ; let is_saturated = tc_args `lengthAtLeast` tyConArity tc
+      = do { let tc_arity = tyConArity tc
+           ; tc_kind <- zonkTcType (tyConKind tc)
+           ; (tc_args, kind) <- tcInstTyBinders (splitPiTysInvisibleN tc_arity tc_kind)
+                 -- Instantiate enough invisible arguments
+                 -- to saturate the family TyCon
+
+           ; let is_saturated = tc_args `lengthAtLeast` tc_arity
                  tc_ty
                    | is_saturated = mkTyConApp tc tc_args `mkNakedCastTy` mkNomReflCo kind
                       -- mkNakedCastTy is for (IT5) of Note [The tcType invariant]
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 8c6133ed27..a5f3295bab 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -38,10 +38,11 @@ import TcClassDcl
 import {-# SOURCE #-} TcInstDcls( tcInstDecls1 )
 import TcDeriv (DerivInfo)
 import TcHsType
+import Inst( tcInstTyBinders )
 import TcMType
+import TcUnify( unifyType )
 import TysWiredIn ( unitTy )
 import TcType
-import Inst( tcInstTyBinders )
 import RnEnv( lookupConstructorFields )
 import FamInst
 import FamInstEnv
@@ -1787,7 +1788,9 @@ tcTyFamInstEqn fam_tc mb_clsinfo
        ; (qtvs, pats, rhs_ty) <- tcFamTyPatsAndGen fam_tc mb_clsinfo
                                       imp_vars (mb_expl_bndrs `orElse` [])
                                       hs_pats
-                                      (tcCheckLHsType rhs_hs_ty)
+                                      (\ res_kind ->
+                                         do { traceTc "tcTyFasmInstEqn" (ppr fam_tc $$ ppr hs_pats $$ ppr res_kind)
+                                            ; tcCheckLHsType rhs_hs_ty res_kind })
 
        ; (ze, qtvs') <- zonkTyBndrs qtvs
        ; pats'       <- zonkTcTypesToTypesX ze pats
@@ -1896,44 +1899,68 @@ tcFamTyPatsAndGen fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats thing_inside
 tcFamTyPats :: TyCon -> Maybe ClsInstInfo
             -> HsTyPats GhcRn                  -- Patterns
             -> TcM ([TcType], TcKind)          -- (pats, rhs_kind)
-tcFamTyPats fam_tc _mb_clsinfo hs_pats
+tcFamTyPats fam_tc mb_clsinfo hs_pats
   = do { traceTc "tcFamTyPats {" $
-         vcat [ ppr fam_tc <+> dcolon <+> ppr fun_kind
+         vcat [ ppr fam_tc <+> dcolon <+> ppr fam_kind
               , text "arity:" <+> ppr fam_arity
-              , text "invis_bndrs:" <+> ppr invis_bndrs ]
-       ; (subst, invis_pats) <- tcInstTyBinders emptyTCvSubst
-                                        -- mb_kind_env
-                                        Nothing
-                                        invis_bndrs
-       ; let fun_ty = mkTyConApp fam_tc invis_pats
+              , text "kind:" <+> ppr fam_kind ]
+
+       ; let fun_ty = mkTyConApp fam_tc []
 
        ; (fam_app, res_kind) <- tcInferApps typeLevelMode lhs_fun fun_ty
-                                            (substTy subst body_kind) hs_pats
+                                            fam_kind hs_pats
 
        ; traceTc "End tcFamTyPats }" $
-         vcat [ ppr fam_tc <+> dcolon <+> ppr fun_kind
+         vcat [ ppr fam_tc <+> dcolon <+> ppr fam_kind
               , text "res_kind:" <+> ppr res_kind ]
 
+       -- Decompose fam_app to get the argument patterns
+       --
        -- We expect fam_app to look like (F t1 .. tn)
        -- tcInferApps is capable of returning ((F ty1 |> co) ty2),
        -- but that can't happen here because we already checked the
        -- arity of F matches the number of pattern
-       ; case splitTyConApp_maybe fam_app of
-           Just (_, pats) -> return  (pats, res_kind)
-           Nothing        -> WARN( True, bad_lhs fam_app )
-                             return ([], res_kind) }
+       ; pats <- case splitTyConApp_maybe fam_app of
+                   Just (_, pats) -> return pats
+                   Nothing        -> WARN( True, bad_lhs fam_app )
+                                     return []
+
+       ; (extra_pats, res_kind) <- tcInstTyBinders $
+                                   splitPiTysInvisible res_kind
+       ; let all_pats = pats ++ extra_pats
+
+       -- Ensure that the instance is consistent its parent class
+       ; addConsistencyConstraints mb_clsinfo fam_tc all_pats
+
+       ; return (all_pats, res_kind) }
   where
     fam_name  = tyConName fam_tc
     fam_arity = tyConArity fam_tc
-    fun_kind  = tyConKind fam_tc
+    fam_kind  = tyConKind fam_tc
     lhs_fun   = noLoc (HsTyVar noExt NotPromoted (noLoc fam_name))
-    (invis_bndrs, body_kind) = splitPiTysInvisibleN fam_arity fun_kind
---     mb_kind_env = thdOf3 <$> mb_clsinfo
 
     bad_lhs fam_app
       = hang (text "Ill-typed LHS of family instance")
            2 (debugPprType fam_app)
 
+addConsistencyConstraints :: Maybe ClsInstInfo -> TyCon -> [Type] -> TcM ()
+-- In the corresponding positions of the class and type-family,
+-- ensure the the family argument is the same as the class argument
+--   E.g    class C a b c d where
+--             F c x y a :: Type
+-- Here the first  arg of F should be the same as the third of C
+--  and the fourth arg of F should be the same as the first of C
+
+addConsistencyConstraints Nothing _ _ = return ()
+addConsistencyConstraints (Just (_, _, inst_ty_env)) fam_tc pats
+  = mapM_ do_one (tyConTyVars fam_tc `zip` pats)
+  where
+    do_one (fam_tc_tv, pat)
+      | Just cls_arg_ty <- lookupVarEnv inst_ty_env fam_tc_tv
+      = discardResult (unifyType Nothing cls_arg_ty pat)
+      | otherwise
+      = return ()
+
 {- Note [Constraints in patterns]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 NB: This isn't the whole story. See comment in tcFamTyPats.
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index ef722653ae..a9bf8db6d3 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -63,6 +63,7 @@ module Type (
         stripCoercionTy, splitCoercionType_maybe,
 
         splitPiTysInvisible, splitPiTysInvisibleN,
+        invisibleTyBndrCount,
         filterOutInvisibleTypes, filterOutInferredTypes,
         partitionInvisibleTypes, partitionInvisibles,
         tyConArgFlags, appTyArgFlags,
@@ -1539,6 +1540,17 @@ splitPiTys ty = split ty ty
                                      in  (Anon arg : bs, ty)
     split orig_ty _                = ([], orig_ty)
 
+invisibleTyBndrCount :: Type -> Int
+-- Returns the number of leading invisible forall'd binders in the type
+invisibleTyBndrCount ty = go ty
+  where
+    go :: Type -> Int
+    go ty               | Just ty' <- coreView ty = go ty'
+    go (ForAllTy b res) | Bndr _ vis <- b
+                        , isInvisibleArgFlag vis  = 1 + go res
+    go (FunTy arg res)  | isPredTy arg            = 1 + go res
+    go _                                          = 0
+
 -- Like splitPiTys, but returns only *invisible* binders, including constraints
 -- Stops at the first visible binder
 splitPiTysInvisible :: Type -> ([TyCoBinder], Type)
@@ -1555,7 +1567,8 @@ splitPiTysInvisible ty = split ty ty []
 
 splitPiTysInvisibleN :: Int -> Type -> ([TyCoBinder], Type)
 -- Same as splitPiTysInvisible, but stop when
--- you have found 'n' TyCoBinders
+--   - you have found 'n' TyCoBinders,
+--   - or you run out of invisible binders
 splitPiTysInvisibleN n ty = split n ty ty []
    where
     split n orig_ty ty bs