Refactor tcInferApps
authorSimon Peyton Jones <simonpj@microsoft.com>
Sun, 3 Sep 2017 11:30:59 +0000 (12:30 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Thu, 14 Sep 2017 07:37:28 +0000 (08:37 +0100)
This is a simple refactor

* Remove an unnecessary accumulating argument (acc_hs_apps) from
  the 'go' function

* And put 'n' first in the same function

compiler/typecheck/TcHsType.hs
testsuite/tests/indexed-types/should_fail/T13877.stderr

index bd73bf3..fdde6f1 100644 (file)
@@ -31,7 +31,7 @@ module TcHsType (
         tcHsLiftedType,   tcHsOpenType,
         tcHsLiftedTypeNC, tcHsOpenTypeNC,
         tcLHsType, tcCheckLHsType,
-        tcHsContext, tcLHsPredType, tcInferApps, tcTyApps,
+        tcHsContext, tcLHsPredType, tcInferApps,
         solveEqualities, -- useful re-export
 
         typeLevelMode, kindLevelMode,
@@ -727,9 +727,9 @@ tcWildCardOcc wc_info exp_kind
 ---------------------------
 -- | Call 'tc_infer_hs_type' and check its result against an expected kind.
 tc_infer_hs_type_ek :: TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
-tc_infer_hs_type_ek mode ty ek
-  = do { (ty', k) <- tc_infer_hs_type mode ty
-       ; checkExpectedKind ty ty' k ek }
+tc_infer_hs_type_ek mode hs_ty ek
+  = do { (ty, k) <- tc_infer_hs_type mode hs_ty
+       ; checkExpectedKind hs_ty ty k ek }
 
 ---------------------------
 tupKindSort_maybe :: TcKind -> Maybe TupleSort
@@ -802,61 +802,63 @@ tcInferApps :: TcTyMode
             -> TcKind               -- ^ Function kind (zonked)
             -> [LHsType GhcRn]      -- ^ Args
             -> TcM (TcType, [TcType], TcKind) -- ^ (f args, args, result kind)
-tcInferApps mode mb_kind_info orig_ty ty ki args
-  = do { traceTc "tcInferApps" (ppr orig_ty $$ ppr args $$ ppr ki)
-       ; go [] [] orig_subst ty orig_ki_binders orig_inner_ki args 1 }
+tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args
+  = do { traceTc "tcInferApps" (ppr orig_hs_ty $$ ppr orig_hs_args $$ ppr fun_ki)
+       ; go 1 [] empty_subst fun_ty orig_ki_binders orig_inner_ki orig_hs_args }
   where
-    orig_subst                       = mkEmptyTCvSubst $ mkInScopeSet $ tyCoVarsOfType ki
-    (orig_ki_binders, orig_inner_ki) = tcSplitPiTys ki
+    empty_subst                      = mkEmptyTCvSubst $ mkInScopeSet $
+                                       tyCoVarsOfType fun_ki
+    (orig_ki_binders, orig_inner_ki) = tcSplitPiTys fun_ki
 
-    go :: [LHsType GhcRn] -- already type-checked args, in reverse order, for errors
+    go :: Int             -- the # of the next argument
        -> [TcType]        -- already type-checked args, in reverse order
        -> TCvSubst        -- instantiating substitution
        -> TcType          -- function applied to some args, could be knot-tied
        -> [TyBinder]      -- binders in function kind (both vis. and invis.)
        -> TcKind          -- function kind body (not a Pi-type)
        -> [LHsType GhcRn] -- un-type-checked args
-       -> Int             -- the # of the next argument
        -> TcM (TcType, [TcType], TcKind)  -- same as overall return type
 
       -- no user-written args left. We're done!
-    go _acc_hs_args acc_args subst fun ki_binders inner_ki [] _
+    go _ acc_args subst fun ki_binders inner_ki []
       = return (fun, reverse acc_args, substTy subst $ mkPiTys ki_binders inner_ki)
 
       -- The function's kind has a binder. Is it visible or invisible?
-    go acc_hs_args acc_args subst fun (ki_binder:ki_binders) inner_ki
-       all_args@(arg:args) n
+    go n acc_args subst fun (ki_binder:ki_binders) inner_ki
+       all_args@(arg:args)
       | isInvisibleBinder ki_binder
         -- It's invisible. Instantiate.
       = do { traceTc "tcInferApps (invis)" (ppr ki_binder $$ ppr subst)
            ; (subst', arg') <- tcInstBinder mb_kind_info subst ki_binder
-           ; go acc_hs_args (arg' : acc_args) subst' (mkNakedAppTy fun arg')
-                ki_binders inner_ki all_args }
+           ; go n (arg' : acc_args) subst' (mkNakedAppTy fun arg')
+                ki_binders inner_ki all_args }
 
       | otherwise
         -- It's visible. Check the next user-written argument
-      = do { traceTc "tcInferApps (vis)" (ppr ki_binder $$ ppr arg $$ ppr subst)
-           ; arg' <- addErrCtxt (funAppCtxt orig_ty arg n) $
+      = do { traceTc "tcInferApps (vis)" (vcat [ ppr ki_binder, ppr arg
+                                               , ppr (tyBinderType ki_binder)
+                                               , ppr subst ])
+           ; arg' <- addErrCtxt (funAppCtxt orig_hs_ty arg n) $
                      tc_lhs_type mode arg (substTy subst $ tyBinderType ki_binder)
            ; let subst' = extendTvSubstBinderAndInScope subst ki_binder arg'
-           ; go (arg : acc_hs_args) (arg' : acc_args) subst' (mkNakedAppTy fun arg')
-                ki_binders inner_ki args (n+1) }
+           ; go (n+1) (arg' : acc_args) subst' (mkNakedAppTy fun arg')
+                ki_binders inner_ki args }
 
        -- We've run out of known binders in the functions's kind.
-    go acc_hs_args acc_args subst fun [] inner_ki all_args n
+    go n acc_args subst fun [] inner_ki all_args
       | not (null new_ki_binders)
          -- But, after substituting, we have more binders.
-      = go acc_hs_args acc_args zapped_subst fun new_ki_binders new_inner_ki all_args n
+      = go n acc_args zapped_subst fun new_ki_binders new_inner_ki all_args
 
       | otherwise
          -- Even after substituting, still no binders. Use matchExpectedFunKind
       = do { traceTc "tcInferApps (no binder)" (ppr new_inner_ki $$ ppr zapped_subst)
            ; (co, arg_k, res_k)
-               <- matchExpectedFunKind (mkHsAppTys orig_ty (reverse acc_hs_args))
+               <- matchExpectedFunKind (mkHsAppTys orig_hs_ty (take (n-1) orig_hs_args))
                                        substed_inner_ki
            ; let subst' = zapped_subst `extendTCvInScopeSet` tyCoVarsOfTypes [arg_k, res_k]
-           ; go acc_hs_args acc_args subst' (fun `mkNakedCastTy` co)
-                [mkAnonBinder arg_k] res_k all_args }
+           ; go n acc_args subst' (fun `mkNakedCastTy` co)
+                [mkAnonBinder arg_k] res_k all_args }
       where
         substed_inner_ki               = substTy subst inner_ki
         (new_ki_binders, new_inner_ki) = tcSplitPiTys substed_inner_ki
@@ -873,8 +875,8 @@ tcTyApps :: TcTyMode
          -> TcKind               -- ^ Function kind (zonked)
          -> [LHsType GhcRn]      -- ^ Args
          -> TcM (TcType, TcKind) -- ^ (f args, result kind)
-tcTyApps mode orig_ty ty ki args
-  = do { (ty', _args, ki') <- tcInferApps mode Nothing orig_ty ty ki args
+tcTyApps mode orig_hs_ty ty ki args
+  = do { (ty', _args, ki') <- tcInferApps mode Nothing orig_hs_ty ty ki args
        ; return (ty', ki') }
 
 --------------------------
@@ -884,7 +886,8 @@ checkExpectedKind :: HsType GhcRn
                   -> TcKind
                   -> TcKind
                   -> TcM TcType
-checkExpectedKind hs_ty ty act exp = fstOf3 <$> checkExpectedKindX Nothing (ppr hs_ty) ty act exp
+checkExpectedKind hs_ty ty act exp
+  = fstOf3 <$> checkExpectedKindX Nothing (ppr hs_ty) ty act exp
 
 checkExpectedKindX :: Maybe (VarEnv Kind)  -- Possibly, instantiations for kind vars
                    -> SDoc                 -- HsType whose kind we're checking
index 4498d97..a90a4dd 100644 (file)
@@ -1,6 +1,6 @@
 
 T13877.hs:65:17: error:
-    • Couldn't match type ‘p xs’ with ‘Apply p xs
+    • Couldn't match type ‘Apply p (x : xs)’ with ‘p (x : xs)
       Expected type: Sing x
                      -> Sing xs -> App [a] (':->) * p xs -> App [a] (':->) * p (x : xs)
         Actual type: Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs)