[project @ 1997-08-25 22:28:07 by sof]
[ghc-hetmet.git] / ghc / compiler / typecheck / Unify.lhs
index ad979b7..cbc42a8 100644 (file)
@@ -11,14 +11,15 @@ updatable substitution).
 
 module Unify ( unifyTauTy, unifyTauTyList, unifyTauTyLists, unifyFunTy ) where
 
-import Ubiq
+IMP_Ubiq()
 
 -- friends: 
 import TcMonad
 import Type    ( GenType(..), typeKind, mkFunTy, getFunTy_maybe )
 import TyCon   ( TyCon, mkFunTyCon )
-import TyVar   ( GenTyVar(..), TyVar(..), tyVarKind )
-import TcType  ( TcType(..), TcMaybe(..), TcTauType(..), TcTyVar(..),
+import Class   ( GenClass )
+import TyVar   ( GenTyVar(..), SYN_IE(TyVar), tyVarKind )
+import TcType  ( SYN_IE(TcType), TcMaybe(..), SYN_IE(TcTauType), SYN_IE(TcTyVar),
                  newTyVarTy, tcReadTyVar, tcWriteTyVar, zonkTcType
                )
 -- others:
@@ -28,6 +29,11 @@ import PprType       ( GenTyVar, GenType )   -- instances
 import Pretty
 import Unique  ( Unique )              -- instances
 import Util
+
+#if __GLASGOW_HASKELL__ >= 202
+import Outputable
+#endif
+
 \end{code}
 
 
@@ -44,7 +50,7 @@ Unify two @TauType@s.  Dead straightforward.
 
 \begin{code}
 unifyTauTy :: TcTauType s -> TcTauType s -> TcM s ()
-unifyTauTy ty1 ty2 
+unifyTauTy ty1 ty2     -- ty1 expected, ty2 inferred
   = tcAddErrCtxtM (unifyCtxt ty1 ty2) $
     uTys ty1 ty1 ty2 ty2
 \end{code}
@@ -59,7 +65,7 @@ unifyTauTyLists :: [TcTauType s] -> [TcTauType s] ->  TcM s ()
 unifyTauTyLists []          []         = returnTc ()
 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2   `thenTc_`
                                        unifyTauTyLists tys1 tys2
-unifyTauTypeLists ty1s ty2s = panic "Unify.unifyTauTypeLists: mismatched type lists!"
+unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
 \end{code}
 
 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
@@ -100,6 +106,7 @@ uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar tyvar2 ps_ty1 ty1
        -- Applications and functions; just check the two parts
 uTys _ (FunTy fun1 arg1 _) _ (FunTy fun2 arg2 _)
   = uTys fun1 fun1 fun2 fun2   `thenTc_`    uTys arg1 arg1 arg2 arg2
+
 uTys _ (AppTy s1 t1) _ (AppTy s2 t2)
   = uTys s1 s1 s2 s2   `thenTc_`    uTys t1 t1 t2 t2
 
@@ -120,10 +127,24 @@ uTys _ (FunTy fun1 arg1 _) _ (AppTy s2 t2)
 uTys ps_ty1 (TyConTy con1 _) ps_ty2 (TyConTy con2 _)
   = checkTc (con1 == con2) (unifyMisMatch ps_ty1 ps_ty2)
 
+       -- Dictionary types must match.  (They can only occur when
+       -- unifying signature contexts in TcBinds.)
+uTys ps_ty1 (DictTy c1 t1 _) ps_ty2 (DictTy c2 t2 _)
+  = checkTc (c1 == c2) (unifyMisMatch ps_ty1 ps_ty2)   `thenTc_`
+    uTys t1 t1 t2 t2
+
        -- Always expand synonyms (see notes at end)
 uTys ps_ty1 (SynTy con1 args1 ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
 uTys ps_ty1 ty1 ps_ty2 (SynTy con2 args2 ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
 
+       -- Not expecting for-alls in unification
+#ifdef DEBUG
+uTys ps_ty1 (ForAllTy _ _)       ps_ty2 ty2 = panic "Unify.uTys:ForAllTy (1st arg)"
+uTys ps_ty1 ty1 ps_ty2       (ForAllTy _ _) = panic "Unify.uTys:ForAllTy (2nd arg)"
+uTys ps_ty1 (ForAllUsageTy _ _ _) ps_ty2 ty2 = panic "Unify.uTys:ForAllUsageTy (1st arg)"
+uTys ps_ty1 ty1 ps_ty2 (ForAllUsageTy _ _ _) = panic "Unify.uTys:ForAllUsageTy (2nd arg)"
+#endif
+
        -- Anything else fails
 uTys ps_ty1 ty1 ps_ty2 ty2  = failTc (unifyMisMatch ps_ty1 ps_ty2)
 \end{code}
@@ -229,15 +250,20 @@ uUnboundVar tv1@(TyVar uniq1 kind1 name1 box1)
     case (maybe_ty1, maybe_ty2) of
        (_, BoundTo ty2') -> uUnboundVar tv1 maybe_ty1 ty2' ty2'
 
-       (DontBind,DontBind) 
-                    -> failTc (unifyDontBindErr tv1 ps_ty2)
-
        (UnBound, _) |  kind2 `hasMoreBoxityInfo` kind1
-                    -> tcWriteTyVar tv1 ty2            `thenNF_Tc_` returnTc ()
+                    -> tcWriteTyVar tv1 ps_ty2         `thenNF_Tc_` returnTc ()
        
        (_, UnBound) |  kind1 `hasMoreBoxityInfo` kind2
                     -> tcWriteTyVar tv2 (TyVarTy tv1)  `thenNF_Tc_` returnTc ()
 
+-- Allow two type-sig variables to be bound together.
+-- They may be from the same binding group, so it may be OK.
+       (DontBind,DontBind) |  kind2 `hasMoreBoxityInfo` kind1
+                           -> tcWriteTyVar tv1 ps_ty2          `thenNF_Tc_` returnTc ()
+       
+                           |  kind1 `hasMoreBoxityInfo` kind2
+                           -> tcWriteTyVar tv2 (TyVarTy tv1)   `thenNF_Tc_` returnTc ()
+
        other        -> failTc (unifyKindErr tv1 ps_ty2)
 
        -- Second one isn't a type variable
@@ -266,7 +292,13 @@ uUnboundVar tv1@(TyVar uniq1 kind1 name1 box1) maybe_ty1 ps_ty2 non_var_ty2
     occur_check (FunTy fun arg _) = occur_check fun `thenTc_` occur_check arg
     occur_check (TyConTy _ _)    = returnTc ()
     occur_check (SynTy _ _ ty2)   = occur_check ty2
-    occur_check other            = panic "Unexpected Dict or ForAll in occurCheck"
+
+       -- DictTys and ForAllTys can occur when pattern matching against
+       -- constructors with universally quantified fields.
+    occur_check (DictTy c ty2 _)  = occur_check ty2
+    occur_check (ForAllTy tv ty2) | tv == tv1 = returnTc ()
+                                 | otherwise = occur_check ty2
+    occur_check other            = panic "Unexpected ForAllUsage in occurCheck"
 \end{code}
 
 %************************************************************************
@@ -310,38 +342,38 @@ Errors
 ~~~~~~
 
 \begin{code}
-unifyCtxt ty1 ty2
+unifyCtxt ty1 ty2              -- ty1 expected, ty2 inferred
   = zonkTcType ty1     `thenNF_Tc` \ ty1' ->
     zonkTcType ty2     `thenNF_Tc` \ ty2' ->
     returnNF_Tc (err ty1' ty2')
   where
-    err ty1' ty2' sty = ppAboves [
-                          ppCat [ppStr "When matching:", ppr sty ty1'],
-                          ppCat [ppStr "      against:", ppr sty ty2']
+    err ty1' ty2' sty = vcat [
+                          hsep [ptext SLIT("Expected:"), ppr sty ty1'],
+                          hsep [ptext SLIT("Inferred:"), ppr sty ty2']
                        ]
 
 unifyMisMatch ty1 ty2 sty
-  = ppHang (ppStr "Couldn't match the type")
-        4 (ppSep [ppr sty ty1, ppStr "against", ppr sty ty2])
+  = hang (ptext SLIT("Couldn't match the type"))
+        4 (sep [ppr sty ty1, ptext SLIT("against"), ppr sty ty2])
 
 expectedFunErr ty sty
-  = ppHang (ppStr "Function type expected, but found the type")
+  = hang (text "Function type expected, but found the type")
         4 (ppr sty ty)
 
 unifyKindErr tyvar ty sty
-  = ppHang (ppStr "Compiler bug: kind mis-match between")
-        4 (ppSep [ppr sty tyvar, ppLparen, ppr sty (tyVarKind tyvar), ppRparen,
-                  ppStr "and", 
-                  ppr sty ty, ppLparen, ppr sty (typeKind ty), ppRparen])
+  = hang (ptext SLIT("Compiler bug: kind mis-match between"))
+        4 (sep [hsep [ppr sty tyvar, ptext SLIT("::"), ppr sty (tyVarKind tyvar)],
+                  ptext SLIT("and"), 
+                  hsep [ppr sty ty, ptext SLIT("::"), ppr sty (typeKind ty)]])
 
 unifyDontBindErr tyvar ty sty
-  = ppHang (ppStr "Couldn't match the *signature/existential* type variable")
-        4 (ppSep [ppr sty tyvar,
-                  ppStr "with the type", 
+  = hang (ptext SLIT("Couldn't match the signature/existential type variable"))
+        4 (sep [ppr sty tyvar,
+                  ptext SLIT("with the type"), 
                   ppr sty ty])
 
 unifyOccurCheck tyvar ty sty
-  = ppHang (ppStr "Cannot construct the infinite type (occur check)")
-        4 (ppSep [ppr sty tyvar, ppStr "=", ppr sty ty])
+  = hang (ptext SLIT("Cannot construct the infinite type (occur check)"))
+        4 (sep [ppr sty tyvar, char '=', ppr sty ty])
 \end{code}