[project @ 2000-04-05 16:25:51 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 f7a78e5..09695e7 100644 (file)
--- a/ghc/compiler/typecheck/TcUnify.lhs
+++ b/ghc/compiler/typecheck/TcUnify.lhs
@@ -16,16 +16,19 @@ module TcUnify ( unifyTauTy, unifyTauTyList, unifyTauTyLists,
 
 -- friends: 
 import TcMonad
-import Type    ( Type(..), tyVarsOfType, funTyCon,
-                 mkFunTy, splitFunTy_maybe, splitTyConApp_maybe,
+import TypeRep ( Type(..), funTyCon,
                  Kind, boxedTypeKind, typeCon, anyBoxCon, anyBoxKind,
+               )  -- friend
+import Type    ( tyVarsOfType,
+                 mkFunTy, splitFunTy_maybe, splitTyConApp_maybe,
+                  isNotUsgTy,
                  splitAppTy_maybe,
                  tidyOpenType, tidyOpenTypes, tidyTyVar
                )
 import TyCon   ( TyCon, isTupleTyCon, isUnboxedTupleTyCon, 
                  tyConArity )
 import Name    ( hasBetterProv )
-import Var     ( TyVar, tyVarKind, varName )
+import Var     ( TyVar, tyVarKind, varName, isSigTyVar )
 import VarEnv  
 import VarSet  ( varSetElems )
 import TcType  ( TcType, TcTauType, TcTyVar, TcKind, 
@@ -126,6 +129,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
 
@@ -250,7 +254,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,13 +275,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
-                  if varName tv1 `hasBetterProv` 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
@@ -286,9 +295,31 @@ 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 non_var_ty2                         `thenNF_Tc_`
+       -- This used to say "ps_ty2" instead of "non_var_ty2"
+
+       -- But that led to an infinite loop in the type checker!
+       -- Consider 
+       --      type A a = ()
+       --
+       --      f :: (A a -> a -> ()) -> ()
+       --      f = \ _ -> ()
+       --
+       --      x :: ()
+       --      x = f (\ x p -> p x)
+       --
+       -- Here, we try to match "t" with "A t", and succeed
+       -- because the unifier looks through synonyms.  The occurs
+       -- check doesn't kick in because we are "really" binding "t" to "()",
+       -- but we *actually* bind "t" to "A t" if we store ps_ty2.
+       -- That leads the typechecker into an infinite loop later.
+
     returnTc ()
   where
     occur_check ty = mapTc occur_check_tv (varSetElems (tyVarsOfType ty))      `thenTc_`
@@ -482,6 +513,13 @@ unifyMisMatch ty1 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_tyvar) = tidyTyVar emptyTidyEnv tyvar
+    (env2, tidy_ty)    = tidyOpenType  env1     ty
+
 unifyOccurCheck tyvar ty
   = (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
              4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))