[project @ 1999-05-28 19:24:26 by simonpj]

[ghc-hetmet.git] / ghc / compiler / typecheck / TcUnify.lhs

diff --git a/ghc/compiler/typecheck/TcUnify.lhs b/ghc/compiler/typecheck/TcUnify.lhs
index a6bf468..c136846 100644 (file)
--- a/ghc/compiler/typecheck/TcUnify.lhs
+++ b/ghc/compiler/typecheck/TcUnify.lhs
@@ -18,14 +18,15 @@ module TcUnify ( unifyTauTy, unifyTauTyList, unifyTauTyLists,
 import TcMonad
 import Type    ( Type(..), tyVarsOfType, funTyCon,
                  mkFunTy, splitFunTy_maybe, splitTyConApp_maybe,
+                  isNotUsgTy,
                  Kind, boxedTypeKind, typeCon, anyBoxCon, anyBoxKind,
                  splitAppTy_maybe,
                  tidyOpenType, tidyOpenTypes, tidyTyVar
                )
 import TyCon   ( TyCon, isTupleTyCon, isUnboxedTupleTyCon, 
                  tyConArity )
-import Name    ( isSysLocalName )
-import Var     ( TyVar, tyVarKind, varName )
+import Name    ( hasBetterProv )
+import Var     ( TyVar, tyVarKind, varName, isSigTyVar )
 import VarEnv  
 import VarSet  ( varSetElems )
 import TcType  ( TcType, TcTauType, TcTyVar, TcKind, 
@@ -126,6 +127,7 @@ uTys :: TcTauType -> TcTauType      -- Error reporting ty1 and real ty1
      -> TcM s ()
 
        -- Always expand synonyms (see notes at end)
+        -- (this also throws away FTVs and usage annots)
 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
 
@@ -141,7 +143,7 @@ uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
        -- Type constructors must match
 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
   = checkTcM (cons_match && length tys1 == length tys2) 
-            (failWithTcM (unifyMisMatch ps_ty1 ps_ty2))                `thenTc_`
+            (unifyMisMatch ps_ty1 ps_ty2)                      `thenTc_`
     unifyTauTyLists tys1 tys2
   where
        -- The AnyBox wild card matches anything
@@ -156,21 +158,21 @@ uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
   = case splitAppTy_maybe ty2 of
        Just (s2,t2) -> uTys s1 s1 s2 s2        `thenTc_`    uTys t1 t1 t2 t2
-       Nothing      -> failWithTcM (unifyMisMatch ps_ty1 ps_ty2)
+       Nothing      -> unifyMisMatch ps_ty1 ps_ty2
 
        -- Now the same, but the other way round
        -- Don't swap the types, because the error messages get worse
 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
   = case splitAppTy_maybe ty1 of
        Just (s1,t1) -> uTys s1 s1 s2 s2        `thenTc_`    uTys t1 t1 t2 t2
-       Nothing      -> failWithTcM (unifyMisMatch ps_ty1 ps_ty2)
+       Nothing      -> unifyMisMatch ps_ty1 ps_ty2
 
        -- Not expecting for-alls in unification
        -- ... but the error message from the unifyMisMatch more informative
        -- than a panic message!
 
        -- Anything else fails
-uTys ps_ty1 ty1 ps_ty2 ty2  = failWithTcM (unifyMisMatch ps_ty1 ps_ty2)
+uTys ps_ty1 ty1 ps_ty2 ty2  = unifyMisMatch ps_ty1 ps_ty2
 \end{code}
 
 Notes on synonyms
@@ -250,7 +252,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
+       -- Expand synonyms; ignore FTVs; ignore usage annots
 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy _ ty2)
   = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
 
@@ -271,14 +273,18 @@ uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
 
        Nothing -> checkKinds swapped tv1 ty2                   `thenTc_`
 
-                       -- Try to update sys-y type variables in preference to sig-y ones
-                       -- (the latter respond False to isSysLocalName)
-                  if isSysLocalName (varName tv2) then
-                       tcPutTyVar tv2 (TyVarTy tv1)                            `thenNF_Tc_`
+                  if tv1 `dominates` tv2 then
+                       tcPutTyVar tv2 (TyVarTy tv1)            `thenNF_Tc_`
                        returnTc ()
                   else
-                       tcPutTyVar tv1 ps_ty2                                   `thenNF_Tc_`
+                        ASSERT( isNotUsgTy ps_ty2 )
+                       tcPutTyVar tv1 ps_ty2                   `thenNF_Tc_`
                        returnTc ()
+  where
+    tv1 `dominates` tv2 =  isSigTyVar tv1 
+                               -- Don't unify a signature type variable if poss
+                       || varName tv1 `hasBetterProv` 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
@@ -287,9 +293,12 @@ uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
   = returnTc ()
 
   | otherwise
-  = checkKinds swapped tv1 non_var_ty2         `thenTc_`
-    occur_check non_var_ty2                    `thenTc_`
-    tcPutTyVar tv1 ps_ty2                      `thenNF_Tc_`
+  = 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_`
+    tcPutTyVar tv1 ps_ty2                              `thenNF_Tc_`
     returnTc ()
   where
     occur_check ty = mapTc occur_check_tv (varSetElems (tyVarsOfType ty))      `thenTc_`
@@ -472,11 +481,23 @@ unifyKindCtxt swapped tv1 ty2 tidy_env    -- not swapped => tv1 expected, ty2 infer
     pp2 = ppr ty2'
 
 unifyMisMatch ty1 ty2
-  = (env2, hang (ptext SLIT("Couldn't match"))
-             4 (sep [quotes (ppr tidy_ty1), ptext SLIT("against"), quotes (ppr tidy_ty2)]))
+  = zonkTcType ty1     `thenNF_Tc` \ ty1' ->
+    zonkTcType ty2     `thenNF_Tc` \ ty2' ->
+    let
+       (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
+       msg = hang (ptext SLIT("Couldn't match"))
+                  4 (sep [quotes (ppr tidy_ty1), 
+                          ptext SLIT("against"), 
+                          quotes (ppr tidy_ty2)])
+    in
+    failWithTcM (env, msg)
+
+unifyWithSigErr tyvar ty
+  = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
+             4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
   where
-    (env1, tidy_ty1) = tidyOpenType emptyTidyEnv ty1
-    (env2, tidy_ty2) = tidyOpenType env1         ty2
+    (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
+    (env2, tidy_ty)    = tidyOpenType  env1     ty
 
 unifyOccurCheck tyvar ty
   = (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))