Add a HsExplicitFlag to SpliceDecl, to improve Trac #4042
[ghc-hetmet.git] / compiler / typecheck / TcUnify.lhs
index 367536b..e038888 100644 (file)
@@ -14,7 +14,6 @@ module TcUnify (
         -- Various unifications
   unifyType, unifyTypeList, unifyTheta,
   unifyKind, unifyKinds, unifyFunKind,
-  checkExpectedKind,
   preSubType, boxyMatchTypes,
 
   --------------------------------
@@ -579,9 +578,10 @@ boxy_match tmpl_tvs orig_tmpl_ty boxy_tvs orig_boxy_ty subst
 
     go ty1 ty2          -- C.f. the isSigmaTy case for boxySubMatchType
         | isSigmaTy ty1
-        , (tvs1, _, tau1) <- tcSplitSigmaTy ty1
-        , (tvs2, _, tau2) <- tcSplitSigmaTy ty2
+        , (tvs1, ps1, tau1) <- tcSplitSigmaTy ty1
+        , (tvs2, ps2, tau2) <- tcSplitSigmaTy ty2
         , equalLength tvs1 tvs2
+        , equalLength ps1  ps2
         = boxy_match (tmpl_tvs `delVarSetList` tvs1)    tau1
                      (boxy_tvs `extendVarSetList` tvs2) tau2 subst
 
@@ -611,7 +611,10 @@ boxy_match tmpl_tvs orig_tmpl_ty boxy_tvs orig_boxy_ty subst
                         Nothing -> orig_boxy_ty
                         Just ty -> ty `boxyLub` orig_boxy_ty
 
-    go _ (TyVarTy tv) | isMetaTyVar tv
+    go _ (TyVarTy tv) | isTcTyVar tv && isMetaTyVar tv
+                               -- NB: A TyVar (not TcTyVar) is possible here, representing
+                               --     a skolem, because in this pure boxy_match function 
+                               --     we don't instantiate foralls to TcTyVars; cf Trac #2714
         = subst         -- Don't fail if the template has more info than the target!
                         -- Otherwise, with tmpl_tvs = [a], matching (a -> Int) ~ (Bool -> beta)
                         -- would fail to instantiate 'a', because the meta-type-variable
@@ -1037,8 +1040,8 @@ lists, when all the elts should be of the same type.
 unifyTypeList :: [TcTauType] -> TcM ()
 unifyTypeList []                 = return ()
 unifyTypeList [_]                = return ()
-unifyTypeList (ty1:tys@(ty2:_)) = do { unifyType ty1 ty2
-                                      ; unifyTypeList tys }
+unifyTypeList (ty1:tys@(ty2:_)) = do { _ <- unifyType ty1 ty2
+                                     ; unifyTypeList tys }
 \end{code}
 
 %************************************************************************
@@ -1085,7 +1088,7 @@ uTysOuter :: InBox -> TcType    -- ty1 is the *actual*   type
           -> TcM CoercionI
 -- We've just pushed a context describing ty1,ty2
 uTysOuter nb1 ty1 nb2 ty2
-        = do { traceTc (text "uTysOuter" <+> ppr ty1 <+> ppr ty2)
+        = do { traceTc (text "uTysOuter" <+> sep [ppr ty1, ppr ty2])
              ; u_tys (Unify True ty1 ty2) nb1 ty1 ty1 nb2 ty2 ty2 }
 
 uTys :: InBox -> TcType -> InBox -> TcType -> TcM CoercionI
@@ -1096,14 +1099,19 @@ uTys nb1 ty1 nb2 ty2
 
 
 --------------
-uTys_s :: InBox -> [TcType]     -- tys1 are the *actual*   types
+uTys_s :: Outer                
+       -> InBox -> [TcType]     -- tys1 are the *actual*   types
        -> InBox -> [TcType]     -- tys2 are the *expected* types
        -> TcM [CoercionI]
-uTys_s _   []         _   []         = return []
-uTys_s nb1 (ty1:tys1) nb2 (ty2:tys2) = do { coi <- uTys nb1 ty1 nb2 ty2
-                                          ; cois <- uTys_s nb1 tys1 nb2 tys2
-                                          ; return (coi:cois) }
-uTys_s _ _ _ _ = panic "Unify.uTys_s: mismatched type lists!"
+uTys_s outer nb1 tys1 nb2 tys2
+  = go tys1 tys2
+  where
+    go []         []         = return []
+    go (ty1:tys1) (ty2:tys2) = do { coi <- uTys nb1 ty1 nb2 ty2
+                                  ; cois <- go tys1 tys2
+                                  ; return (coi:cois) }
+    go _ _ = unifyMisMatch outer
+       -- See Note [Mismatched type lists and application decomposition]
 
 --------------
 u_tys :: Outer
@@ -1192,15 +1200,17 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
     go outer _ (PredTy p1) _ (PredTy p2)
         = uPred outer nb1 p1 nb2 p2
 
-        -- Type constructors must match
-    go _ _ (TyConApp con1 tys1) _ (TyConApp con2 tys2)
+        -- Non-synonym type constructors must match
+    go outer _ (TyConApp con1 tys1) _ (TyConApp con2 tys2)
       | con1 == con2 && not (isOpenSynTyCon con1)
-      = do { cois <- uTys_s nb1 tys1 nb2 tys2
+      = do { traceTc (text "utys1" <+> ppr con1 <+> (ppr tys1 $$ ppr tys2))
+           ; cois <- uTys_s outer nb1 tys1 nb2 tys2
            ; return $ mkTyConAppCoI con1 tys1 cois
            }
-        -- See Note [TyCon app]
+        -- Family synonyms See Note [TyCon app]
       | con1 == con2 && identicalOpenSynTyConApp
-      = do { cois <- uTys_s nb1 tys1' nb2 tys2'
+      = do { traceTc (text "utys2" <+> ppr con1 <+> (ppr tys1' $$ ppr tys2'))
+           ; cois <- uTys_s outer nb1 tys1' nb2 tys2'
            ; return $ mkTyConAppCoI con1 tys1 (replicate n IdCo ++ cois)
            }
       where
@@ -1221,9 +1231,10 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
         -- NB: we've already dealt with type variables and Notes,
         -- so if one type is an App the other one jolly well better be too
+        -- See Note [Mismatched type lists and application decomposition]
     go outer _ (AppTy s1 t1) _ ty2
       | Just (s2,t2) <- tcSplitAppTy_maybe ty2
-      = do { coi_s <- go outer s1 s1 s2 s2      -- NB recurse into go
+      = do { coi_s <- go outer s1 s1 s2 s2      -- NB recurse into go...
            ; coi_t <- uTys nb1 t1 nb2 t2        -- See Note [Unifying AppTy]
            ; return $ mkAppTyCoI s1 coi_s t1 coi_t }
 
@@ -1235,48 +1246,47 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
            ; coi_t <- uTys nb1 t1 nb2 t2
            ; return $ mkAppTyCoI s1 coi_s t1 coi_t }
 
-        -- One or both outermost constructors are type family applications.
-        -- If we can normalise them away, proceed as usual; otherwise, we
-        -- need to defer unification by generating a wanted equality constraint.
-    go outer sty1 ty1 sty2 ty2
-      | ty1_is_fun || ty2_is_fun
-      = do { (coi1, ty1') <- if ty1_is_fun then tcNormaliseFamInst ty1
-                                           else return (IdCo, ty1)
-           ; (coi2, ty2') <- if ty2_is_fun then tcNormaliseFamInst ty2
-                                           else return (IdCo, ty2)
-           ; coi <- if isOpenSynTyConApp ty1' || isOpenSynTyConApp ty2'
-                    then do { -- One type family app can't be reduced yet
-                              -- => defer
-                            ; ty1'' <- zonkTcType ty1'
-                            ; ty2'' <- zonkTcType ty2'
-                            ; if tcEqType ty1'' ty2''
-                              then return IdCo
-                              else -- see [Deferred Unification]
-                                defer_unification outer False orig_ty1 orig_ty2
-                            }
-                     else -- unification can proceed
-                          go outer sty1 ty1' sty2 ty2'
-           ; return $ coi1 `mkTransCoI` coi `mkTransCoI` (mkSymCoI coi2)
+        -- If we can reduce a family app => proceed with reduct
+        -- NB1: We use isOpenSynTyCon, not isOpenSynTyConApp as we also must
+        --      defer oversaturated applications!
+       -- 
+       -- NB2: Do this *after* trying decomposing applications, so that decompose
+       --        (m a) ~ (F Int b)
+       --      where F has arity 1
+    go _ _ ty1@(TyConApp con1 _) _ ty2
+      | isOpenSynTyCon con1
+      = do { (coi1, ty1') <- tcNormaliseFamInst ty1
+           ; case coi1 of
+               IdCo -> defer    -- no reduction, see [Deferred Unification]
+               _    -> liftM (coi1 `mkTransCoI`) $ uTys nb1 ty1' nb2 ty2
+           }
+
+    go _ _ ty1 _ ty2@(TyConApp con2 _)
+      | isOpenSynTyCon con2
+      = do { (coi2, ty2') <- tcNormaliseFamInst ty2
+           ; case coi2 of
+               IdCo -> defer    -- no reduction, see [Deferred Unification]
+               _    -> liftM (`mkTransCoI` mkSymCoI coi2) $ 
+                       uTys nb1 ty1 nb2 ty2'
            }
-        where
-          ty1_is_fun = isOpenSynTyConApp ty1
-          ty2_is_fun = isOpenSynTyConApp ty2
 
         -- Anything else fails
     go outer _ _ _ _ = bale_out outer
 
+    defer = defer_unification outer False orig_ty1 orig_ty2
+
+
 ----------
 uPred :: Outer -> InBox -> PredType -> InBox -> PredType -> TcM CoercionI
 uPred _ nb1 (IParam n1 t1) nb2 (IParam n2 t2)
-  | n1 == n2 =
-        do { coi <- uTys nb1 t1 nb2 t2
-           ; return $ mkIParamPredCoI n1 coi
-           }
-uPred _ nb1 (ClassP c1 tys1) nb2 (ClassP c2 tys2)
-  | c1 == c2 =
-        do { cois <- uTys_s nb1 tys1 nb2 tys2           -- Guaranteed equal lengths because the kinds check
-           ; return $ mkClassPPredCoI c1 tys1 cois
-           }
+  | n1 == n2
+  = do { coi <- uTys nb1 t1 nb2 t2
+       ; return $ mkIParamPredCoI n1 coi }
+uPred outer nb1 (ClassP c1 tys1) nb2 (ClassP c2 tys2)
+  | c1 == c2
+  = do { traceTc (text "utys3" <+> ppr c1 <+> (ppr tys2 $$ ppr tys2))
+       ; cois <- uTys_s outer nb1 tys1 nb2 tys2
+       ; return $ mkClassPPredCoI c1 tys1 cois }
 uPred outer _ _ _ _ = unifyMisMatch outer
 
 uPreds :: Outer -> InBox -> [PredType] -> InBox -> [PredType]
@@ -1290,15 +1300,23 @@ uPreds outer nb1 (p1:ps1) nb2 (p2:ps2) =
 uPreds _ _ _ _ _ = panic "uPreds"
 \end{code}
 
-Note [TyCon app]
-~~~~~~~~~~~~~~~~
-When we find two TyConApps, the argument lists are guaranteed equal
-length.  Reason: intially the kinds of the two types to be unified is
-the same. The only way it can become not the same is when unifying two
-AppTys (f1 a1):=:(f2 a2).  In that case there can't be a TyConApp in
-the f1,f2 (because it'd absorb the app).  If we unify f1:=:f2 first,
-which we do, that ensures that f1,f2 have the same kind; and that
-means a1,a2 have the same kind.  And now the argument repeats.
+Note [Mismatched type lists and application decomposition]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When we find two TyConApps, you might think that the argument lists 
+are guaranteed equal length.  But they aren't. Consider matching
+       w (T x) ~ Foo (T x y)
+We do match (w ~ Foo) first, but in some circumstances we simply create
+a deferred constraint; and then go ahead and match (T x ~ T x y).
+This came up in Trac #3950.
+
+So either 
+   (a) either we must check for identical argument kinds 
+       when decomposing applications,
+  
+   (b) or we must be prepared for ill-kinded unification sub-problems
+
+Currently we adopt (b) since it seems more robust -- no need to maintain
+a global invariant.
 
 Note [OpenSynTyCon app]
 ~~~~~~~~~~~~~~~~~~~~~~~
@@ -1680,7 +1698,7 @@ zapToMonotype :: BoxySigmaType -> TcM TcTauType
 -- with that type.
 zapToMonotype res_ty
   = do  { res_tau <- newFlexiTyVarTy liftedTypeKind
-        ; boxyUnify res_tau res_ty
+        ; _ <- boxyUnify res_tau res_ty
         ; return res_tau }
 
 unBox :: BoxyType -> TcM TcType
@@ -1871,7 +1889,7 @@ kindSimpleKind :: Bool -> Kind -> TcM SimpleKind
 -- (kindSimpleKind True k) returns a simple kind sk such that sk <: k
 -- If the flag is False, it requires k <: sk
 -- E.g.         kindSimpleKind False ?? = *
--- What about (kv -> *) :=: ?? -> *
+-- What about (kv -> *) ~ ?? -> *
 kindSimpleKind orig_swapped orig_kind
   = go orig_swapped orig_kind
   where
@@ -1919,75 +1937,6 @@ unifyFunKind _                         = return Nothing
 
 %************************************************************************
 %*                                                                      *
-        Checking kinds
-%*                                                                      *
-%************************************************************************
-
----------------------------
--- We would like to get a decent error message from
---   (a) Under-applied type constructors
---              f :: (Maybe, Maybe)
---   (b) Over-applied type constructors
---              f :: Int x -> Int x
---
-
-\begin{code}
-checkExpectedKind :: Outputable a => a -> TcKind -> TcKind -> TcM ()
--- A fancy wrapper for 'unifyKind', which tries
--- to give decent error messages.
---      (checkExpectedKind ty act_kind exp_kind)
--- checks that the actual kind act_kind is compatible
---      with the expected kind exp_kind
--- The first argument, ty, is used only in the error message generation
-checkExpectedKind ty act_kind exp_kind
-  | act_kind `isSubKind` exp_kind -- Short cut for a very common case
-  = return ()
-  | otherwise = do
-    (_errs, mb_r) <- tryTc (unifyKind exp_kind act_kind)
-    case mb_r of
-        Just _  -> return ()  -- Unification succeeded
-        Nothing -> do
-
-        -- So there's definitely an error
-        -- Now to find out what sort
-           exp_kind <- zonkTcKind exp_kind
-           act_kind <- zonkTcKind act_kind
-
-           env0 <- tcInitTidyEnv
-           let (exp_as, _) = splitKindFunTys exp_kind
-               (act_as, _) = splitKindFunTys act_kind
-               n_exp_as = length exp_as
-               n_act_as = length act_as
-
-               (env1, tidy_exp_kind) = tidyKind env0 exp_kind
-               (env2, tidy_act_kind) = tidyKind env1 act_kind
-
-               err | n_exp_as < n_act_as     -- E.g. [Maybe]
-                   = quotes (ppr ty) <+> ptext (sLit "is not applied to enough type arguments")
-
-                     -- Now n_exp_as >= n_act_as. In the next two cases,
-                     -- n_exp_as == 0, and hence so is n_act_as
-                   | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
-                   = ptext (sLit "Expecting a lifted type, but") <+> quotes (ppr ty)
-                       <+> ptext (sLit "is unlifted")
-
-                   | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind
-                   = ptext (sLit "Expecting an unlifted type, but") <+> quotes (ppr ty)
-                       <+> ptext (sLit "is lifted")
-
-                   | otherwise               -- E.g. Monad [Int]
-                   = ptext (sLit "Kind mis-match")
-
-               more_info = sep [ ptext (sLit "Expected kind") <+>
-                                     quotes (pprKind tidy_exp_kind) <> comma,
-                                 ptext (sLit "but") <+> quotes (ppr ty) <+>
-                                     ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind)]
-
-           failWithTcM (env2, err $$ more_info)
-\end{code}
-
-%************************************************************************
-%*                                                                      *
 \subsection{Checking signature type variables}
 %*                                                                      *
 %************************************************************************
@@ -2039,7 +1988,7 @@ check_sig_tyvars
 check_sig_tyvars _ []
   = return ()
 check_sig_tyvars extra_tvs sig_tvs
-  = ASSERT( all isSkolemTyVar sig_tvs )
+  = ASSERT( all isTcTyVar sig_tvs && all isSkolemTyVar sig_tvs )
     do  { gbl_tvs <- tcGetGlobalTyVars
         ; traceTc (text "check_sig_tyvars" <+> (vcat [text "sig_tys" <+> ppr sig_tvs,
                                       text "gbl_tvs" <+> ppr gbl_tvs,