[project @ 2001-01-29 08:42:54 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcUnify.lhs
index 7c92681..b732b0d 100644 (file)
@@ -16,21 +16,21 @@ module TcUnify ( unifyTauTy, unifyTauTyList, unifyTauTyLists,
 
 -- friends: 
 import TcMonad
-import TypeRep ( Type(..) )  -- friend
-import Type    ( funTyCon, Kind, unboxedTypeKind, boxedTypeKind, openTypeKind, 
-                 superBoxity, typeCon, openKindCon, hasMoreBoxityInfo, 
+import TypeRep ( Type(..), PredType(..) )  -- friend
+import Type    ( unliftedTypeKind, liftedTypeKind, openTypeKind, 
+                 typeCon, openKindCon, hasMoreBoxityInfo, 
                  tyVarsOfType, typeKind,
-                 mkTyVarTy, mkFunTy, splitFunTy_maybe, splitTyConApp_maybe,
-                  isNotUsgTy, splitAppTy_maybe, mkTyConApp, 
+                 mkFunTy, splitFunTy_maybe, splitTyConApp_maybe,
+                  splitAppTy_maybe, mkTyConApp, 
                  tidyOpenType, tidyOpenTypes, tidyTyVar
                )
 import TyCon   ( TyCon, isTupleTyCon, tupleTyConBoxity, tyConArity )
-import Name    ( hasBetterProv )
-import Var     ( TyVar, tyVarKind, varName, isSigTyVar )
+import Var     ( tyVarKind, varName, isSigTyVar )
 import VarSet  ( varSetElems )
 import TcType  ( TcType, TcTauType, TcTyVar, TcKind, newBoxityVar,
                  newTyVarTy, newTyVarTys, tcGetTyVar, tcPutTyVar, zonkTcType
                )
+import Name    ( isSystemName )
 
 -- others:
 import BasicTypes ( Arity, Boxity, isBoxed )
@@ -48,12 +48,12 @@ import Outputable
 \begin{code}
 unifyKind :: TcKind                -- Expected
          -> TcKind                 -- Actual
-         -> TcM s ()
+         -> TcM ()
 unifyKind k1 k2 
   = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $
     uTys k1 k1 k2 k2
 
-unifyKinds :: [TcKind] -> [TcKind] -> TcM s ()
+unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
 unifyKinds []       []       = returnTc ()
 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2         `thenTc_`
                               unifyKinds ks1 ks2
@@ -61,7 +61,7 @@ unifyKinds _ _ = panic "unifyKinds: length mis-match"
 \end{code}
 
 \begin{code}
-unifyOpenTypeKind :: TcKind -> TcM s ()        
+unifyOpenTypeKind :: TcKind -> TcM ()  
 -- Ensures that the argument kind is of the form (Type bx)
 -- for some boxity bx
 
@@ -94,7 +94,7 @@ non-exported generic functions.
 Unify two @TauType@s.  Dead straightforward.
 
 \begin{code}
-unifyTauTy :: TcTauType -> TcTauType -> TcM s ()
+unifyTauTy :: TcTauType -> TcTauType -> TcM ()
 unifyTauTy ty1 ty2     -- ty1 expected, ty2 inferred
   = tcAddErrCtxtM (unifyCtxt "type" ty1 ty2) $
     uTys ty1 ty1 ty2 ty2
@@ -106,7 +106,7 @@ of equal length.  We charge down the list explicitly so that we can
 complain if their lengths differ.
 
 \begin{code}
-unifyTauTyLists :: [TcTauType] -> [TcTauType] ->  TcM s ()
+unifyTauTyLists :: [TcTauType] -> [TcTauType] ->  TcM ()
 unifyTauTyLists []          []         = returnTc ()
 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2   `thenTc_`
                                        unifyTauTyLists tys1 tys2
@@ -118,7 +118,7 @@ all together.  It is used, for example, when typechecking explicit
 lists, when all the elts should be of the same type.
 
 \begin{code}
-unifyTauTyList :: [TcTauType] -> TcM s ()
+unifyTauTyList :: [TcTauType] -> TcM ()
 unifyTauTyList []               = returnTc ()
 unifyTauTyList [ty]             = returnTc ()
 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2  `thenTc_`
@@ -145,18 +145,28 @@ uTys :: TcTauType -> TcTauType    -- Error reporting ty1 and real ty1
 
      -> TcTauType -> TcTauType -- Error reporting ty2 and real ty2
                                -- ty2 is the *actual* type
-     -> TcM s ()
+     -> TcM ()
 
        -- Always expand synonyms (see notes at end)
-        -- (this also throws away FTVs and usage annots)
+        -- (this also throws away FTVs)
 uTys ps_ty1 (NoteTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
 uTys ps_ty1 ty1 ps_ty2 (NoteTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
 
+       -- Ignore usage annotations inside typechecker
+uTys ps_ty1 (UsageTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
+uTys ps_ty1 ty1 ps_ty2 (UsageTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
+
        -- Variables; go for uVar
 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True  tyvar2 ps_ty1 ty1
                                        -- "True" means args swapped
 
+       -- Predicates
+uTys _ (PredTy (IParam n1 t1)) _ (PredTy (IParam n2 t2))
+  | n1 == n2 = uTys t1 t1 t2 t2
+uTys _ (PredTy (Class c1 tys1)) _ (PredTy (Class c2 tys2))
+  | c1 == c2 = unifyTauTyLists tys1 tys2
+
        -- Functions; just check the two parts
 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
   = uTys fun1 fun1 fun2 fun2   `thenTc_`    uTys arg1 arg1 arg2 arg2
@@ -172,10 +182,6 @@ uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
        -- (CCallable Int) and (CCallable Int#) are both OK
   = unifyOpenTypeKind ps_ty2
 
-  | otherwise
-  = unifyMisMatch ps_ty1 ps_ty2
-
-
        -- Applications need a bit of care!
        -- They can match FunTy and TyConApp, so use splitAppTy_maybe
        -- NB: we've already dealt with type variables and Notes,
@@ -268,7 +274,7 @@ uVar :: Bool                -- False => tyvar is the "expected"
                        -- True  => ty    is the "expected" thing
      -> TcTyVar
      -> TcTauType -> TcTauType -- printing and real versions
-     -> TcM s ()
+     -> TcM ()
 
 uVar swapped tv1 ps_ty2 ty2
   = tcGetTyVar tv1     `thenNF_Tc` \ maybe_ty1 ->
@@ -277,7 +283,7 @@ uVar swapped tv1 ps_ty2 ty2
                 | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
        other       -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
 
-       -- Expand synonyms; ignore FTVs; ignore usage annots
+       -- Expand synonyms; ignore FTVs
 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy _ ty2)
   = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
 
@@ -296,7 +302,7 @@ uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
     case maybe_ty2 of
        Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
 
-       Nothing | tv1_dominates_tv2 
+       Nothing | update_tv2
 
                -> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
                   tcPutTyVar tv2 (TyVarTy tv1)         `thenNF_Tc_`
@@ -304,29 +310,30 @@ uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
                |  otherwise
 
                -> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
-                   (ASSERT( isNotUsgTy ps_ty2 )
-                   tcPutTyVar tv1 ps_ty2               `thenNF_Tc_`
+                   (tcPutTyVar tv1 ps_ty2              `thenNF_Tc_`
                    returnTc ())
   where
     k1 = tyVarKind tv1
     k2 = tyVarKind tv2
-    tv1_dominates_tv2 =    isSigTyVar tv1 
+    update_tv2 = (k2 == openTypeKind) || (k1 /= openTypeKind && nicer_to_update_tv2)
+                       -- Try to get rid of open type variables as soon as poss
+
+    nicer_to_update_tv2 =  isSigTyVar tv1 
                                -- Don't unify a signature type variable if poss
-                       || k2 == openTypeKind
-                               -- Try to get rid of open type variables as soon as poss
-                       || varName tv1 `hasBetterProv` varName tv2 
+                       || isSystemName (varName tv2)
                                -- Try to update sys-y type variables in preference to sig-y ones
 
        -- Second one isn't a type variable
 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
   = checkKinds swapped tv1 non_var_ty2                 `thenTc_`
     occur_check non_var_ty2                            `thenTc_`
-    ASSERT( isNotUsgTy ps_ty2 )
     checkTcM (not (isSigTyVar tv1))
             (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_`
 
-    WARN( not (typeKind non_var_ty2 `hasMoreBoxityInfo` tyVarKind tv1), (ppr tv1 <+> ppr (tyVarKind tv1)) $$
-                                                                       (ppr non_var_ty2 <+> ppr (typeKind non_var_ty2)) )
+    warnTc (not (typeKind non_var_ty2 `hasMoreBoxityInfo` tyVarKind tv1))
+          ((ppr tv1 <+> ppr (tyVarKind tv1)) $$ 
+            (ppr non_var_ty2 <+> ppr (typeKind non_var_ty2)))          `thenNF_Tc_` 
+
     tcPutTyVar tv1 non_var_ty2                         `thenNF_Tc_`
        -- This used to say "ps_ty2" instead of "non_var_ty2"
 
@@ -364,9 +371,9 @@ uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
 
 checkKinds swapped tv1 ty2
 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
--- We need to check that we don't unify a boxed type variable with an
--- unboxed type: e.g.  (id 3#) is illegal
-  | tk1 == boxedTypeKind && tk2 == unboxedTypeKind
+-- We need to check that we don't unify a lifted type variable with an
+-- unlifted type: e.g.  (id 3#) is illegal
+  | tk1 == liftedTypeKind && tk2 == unliftedTypeKind
   = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2)      $
     unifyMisMatch k1 k2
   | otherwise
@@ -389,7 +396,7 @@ checkKinds swapped tv1 ty2
 
 \begin{code}
 unifyFunTy :: TcType                           -- Fail if ty isn't a function type
-          -> TcM s (TcType, TcType)    -- otherwise return arg and result types
+          -> TcM (TcType, TcType)      -- otherwise return arg and result types
 
 unifyFunTy ty@(TyVarTy tyvar)
   = tcGetTyVar tyvar   `thenNF_Tc` \ maybe_ty ->
@@ -411,7 +418,7 @@ unify_fun_ty_help ty        -- Special cases failed, so revert to ordinary unification
 
 \begin{code}
 unifyListTy :: TcType              -- expected list type
-           -> TcM s TcType      -- list element type
+           -> TcM TcType      -- list element type
 
 unifyListTy ty@(TyVarTy tyvar)
   = tcGetTyVar tyvar   `thenNF_Tc` \ maybe_ty ->
@@ -425,13 +432,13 @@ unifyListTy ty
        other                                       -> unify_list_ty_help ty
 
 unify_list_ty_help ty  -- Revert to ordinary unification
-  = newTyVarTy boxedTypeKind           `thenNF_Tc` \ elt_ty ->
+  = newTyVarTy liftedTypeKind          `thenNF_Tc` \ elt_ty ->
     unifyTauTy ty (mkListTy elt_ty)    `thenTc_`
     returnTc elt_ty
 \end{code}
 
 \begin{code}
-unifyTupleTy :: Boxity -> Arity -> TcType -> TcM s [TcType]
+unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType]
 unifyTupleTy boxity arity ty@(TyVarTy tyvar)
   = tcGetTyVar tyvar   `thenNF_Tc` \ maybe_ty ->
     case maybe_ty of
@@ -452,7 +459,7 @@ unify_tuple_ty_help boxity arity ty
     unifyTauTy ty (mkTupleTy boxity arity arg_tys)     `thenTc_`
     returnTc arg_tys
   where
-    kind | isBoxed boxity = boxedTypeKind
+    kind | isBoxed boxity = liftedTypeKind
         | otherwise      = openTypeKind
 \end{code}