Make a smart mkAppTyM
[ghc.git] / compiler / typecheck / TcUnify.hs
index 05a30fd..6af873e 100644 (file)
@@ -14,7 +14,7 @@ module TcUnify (
   tcSubTypeHR, tcSubTypeO, tcSubType_NC, tcSubTypeDS,
   tcSubTypeDS_NC_O, tcSubTypeET,
   checkConstraints, checkTvConstraints,
-  buildImplicationFor,
+  buildImplicationFor, emitResidualTvConstraint,
 
   -- Various unifications
   unifyType, unifyKind,
@@ -440,7 +440,7 @@ matchExpectedAppTy orig_ty
            ; co <- unifyType Nothing (mkAppTy ty1 ty2) orig_ty
            ; return (co, (ty1, ty2)) }
 
-    orig_kind = typeKind orig_ty
+    orig_kind = tcTypeKind orig_ty
     kind1 = mkFunTy liftedTypeKind orig_kind
     kind2 = liftedTypeKind    -- m :: * -> k
                               -- arg type :: *
@@ -790,7 +790,7 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
 
     inst_and_unify = do { (wrap, rho_a) <- deeplyInstantiate inst_orig ty_actual
 
-                           -- if we haven't recurred through an arrow, then
+                           -- If we haven't recurred through an arrow, then
                            -- the eq_orig will list ty_actual. In this case,
                            -- we want to update the origin to reflect the
                            -- instantiation. If we *have* recurred through
@@ -911,7 +911,7 @@ fill_infer_result orig_ty (IR { ir_uniq = u, ir_lvl = res_lvl
       = do { let ty_lvl = tcTypeLevel ty
            ; MASSERT2( not (ty_lvl `strictlyDeeperThan` res_lvl),
                        ppr u $$ ppr res_lvl $$ ppr ty_lvl $$
-                       ppr ty <+> dcolon <+> ppr (typeKind ty) $$ ppr orig_ty )
+                       ppr ty <+> dcolon <+> ppr (tcTypeKind ty) $$ ppr orig_ty )
            ; cts <- readTcRef ref
            ; case cts of
                Just already_there -> pprPanic "writeExpType"
@@ -993,12 +993,12 @@ promoteTcType dest_lvl ty
     dont_promote_it :: TcM (TcCoercion, TcType)
     dont_promote_it  -- Check that ty :: TYPE rr, for some (fresh) rr
       = do { res_kind <- newOpenTypeKind
-           ; let ty_kind = typeKind ty
+           ; let ty_kind = tcTypeKind ty
                  kind_orig = TypeEqOrigin { uo_actual   = ty_kind
                                           , uo_expected = res_kind
                                           , uo_thing    = Nothing
                                           , uo_visible  = False }
-           ; ki_co <- uType KindLevel kind_orig (typeKind ty) res_kind
+           ; ki_co <- uType KindLevel kind_orig (tcTypeKind ty) res_kind
            ; let co = mkTcGReflRightCo Nominal ty ki_co
            ; return (co, ty `mkCastTy` ki_co) }
 
@@ -1167,20 +1167,27 @@ checkTvConstraints skol_info m_telescope thing_inside
   = do { (tclvl, wanted, (skol_tvs, result))
              <- pushLevelAndCaptureConstraints thing_inside
 
-       ; if isEmptyWC wanted
-         then return ()
-         else do { ev_binds <- newNoTcEvBinds
-                 ; implic   <- newImplication
-                 ; emitImplication $
-                   implic { ic_tclvl     = tclvl
-                          , ic_skols     = skol_tvs
-                          , ic_no_eqs    = True
-                          , ic_telescope = m_telescope
-                          , ic_wanted    = wanted
-                          , ic_binds     = ev_binds
-                          , ic_info      = skol_info } }
+       ; emitResidualTvConstraint skol_info m_telescope
+                                  skol_tvs tclvl wanted
+
        ; return (skol_tvs, result) }
 
+emitResidualTvConstraint :: SkolemInfo -> Maybe SDoc -> [TcTyVar]
+                         -> TcLevel -> WantedConstraints -> TcM ()
+emitResidualTvConstraint skol_info m_telescope skol_tvs tclvl wanted
+  | isEmptyWC wanted
+  = return ()
+  | otherwise
+  = do { ev_binds <- newNoTcEvBinds
+       ; implic   <- newImplication
+       ; emitImplication $
+         implic { ic_tclvl     = tclvl
+                , ic_skols     = skol_tvs
+                , ic_no_eqs    = True
+                , ic_telescope = m_telescope
+                , ic_wanted    = wanted
+                , ic_binds     = ev_binds
+                , ic_info      = skol_info } }
 
 implicationNeeded :: SkolemInfo -> [TcTyVar] -> [EvVar] -> TcM Bool
 -- See Note [When to build an implication]
@@ -1443,12 +1450,12 @@ uType t_or_k origin orig_ty1 orig_ty2
 
     go (AppTy s1 t1) (TyConApp tc2 ts2)
       | Just (ts2', t2') <- snocView ts2
-      = ASSERT( mightBeUnsaturatedTyCon tc2 )
+      = ASSERT( not (mustBeSaturated tc2) )
         go_app (isNextTyConArgVisible tc2 ts2') s1 t1 (TyConApp tc2 ts2') t2'
 
     go (TyConApp tc1 ts1) (AppTy s2 t2)
       | Just (ts1', t1') <- snocView ts1
-      = ASSERT( mightBeUnsaturatedTyCon tc1 )
+      = ASSERT( not (mustBeSaturated tc1) )
         go_app (isNextTyConArgVisible tc1 ts1') (TyConApp tc1 ts1') t1' s2 t2
 
     go (CoercionTy co1) (CoercionTy co2)
@@ -1632,10 +1639,10 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
     go dflags cur_lvl
       | canSolveByUnification cur_lvl tv1 ty2
       , Just ty2' <- metaTyVarUpdateOK dflags tv1 ty2
-      = do { co_k <- uType KindLevel kind_origin (typeKind ty2') (tyVarKind tv1)
+      = do { co_k <- uType KindLevel kind_origin (tcTypeKind ty2') (tyVarKind tv1)
            ; traceTc "uUnfilledVar2 ok" $
              vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
-                  , ppr ty2 <+> dcolon <+> ppr (typeKind  ty2)
+                  , ppr ty2 <+> dcolon <+> ppr (tcTypeKind  ty2)
                   , ppr (isTcReflCo co_k), ppr co_k ]
 
            ; if isTcReflCo co_k  -- only proceed if the kinds matched.
@@ -2012,37 +2019,43 @@ we return a made-up TcTyVarDetails, but I think it works smoothly.
 -}
 
 -- | Breaks apart a function kind into its pieces.
-matchExpectedFunKind :: Outputable fun
-                     => fun             -- ^ type, only for errors
-                     -> TcKind          -- ^ function kind
-                     -> TcM (Coercion, TcKind, TcKind)
-                                  -- ^ co :: old_kind ~ arg -> res
-matchExpectedFunKind hs_ty = go
+matchExpectedFunKind
+  :: Outputable fun
+  => fun             -- ^ type, only for errors
+  -> Arity           -- ^ n: number of desired arrows
+  -> TcKind          -- ^ fun_ kind
+  -> TcM Coercion    -- ^ co :: fun_kind ~ (arg1 -> ... -> argn -> res)
+
+matchExpectedFunKind hs_ty n k = go n k
   where
-    go k | Just k' <- tcView k = go k'
+    go 0 k = return (mkNomReflCo k)
+
+    go n k | Just k' <- tcView k = go n k'
 
-    go k@(TyVarTy kvar)
+    go k@(TyVarTy kvar)
       | isMetaTyVar kvar
       = do { maybe_kind <- readMetaTyVar kvar
            ; case maybe_kind of
-                Indirect fun_kind -> go fun_kind
-                Flexi ->             defer k }
+                Indirect fun_kind -> go fun_kind
+                Flexi ->             defer k }
 
-    go k@(FunTy arg res) = return (mkNomReflCo k, arg, res)
-    go other             = defer other
+    go n (FunTy arg res)
+      = do { co <- go (n-1) res
+           ; return (mkTcFunCo Nominal (mkTcNomReflCo arg) co) }
 
-    defer k
-      = do { arg_kind <- newMetaKindVar
-           ; res_kind <- newMetaKindVar
-           ; let new_fun = mkFunTy arg_kind res_kind
+    go n other
+     = defer n other
+
+    defer n k
+      = do { arg_kinds <- newMetaKindVars n
+           ; res_kind  <- newMetaKindVar
+           ; let new_fun = mkFunTys arg_kinds res_kind
                  origin  = TypeEqOrigin { uo_actual   = k
                                         , uo_expected = new_fun
                                         , uo_thing    = Just (ppr hs_ty)
                                         , uo_visible  = True
                                         }
-           ; co <- uType KindLevel origin k new_fun
-           ; return (co, arg_kind, res_kind) }
-
+           ; uType KindLevel origin k new_fun }
 
 {- *********************************************************************
 *                                                                      *