\begin{code}
#include "HsVersions.h"
-module Unify ( unifyTauTy, unifyTauTyList, unifyTauTyLists ) where
+module Unify ( unifyTauTy, unifyTauTyList, unifyTauTyLists, unifyFunTy ) where
-import Ubiq
+IMP_Ubiq()
-- friends:
import TcMonad
-import Type ( GenType(..), getTypeKind )
-import TyCon ( TyCon(..), ConsVisible, NewOrData )
-import TyVar ( GenTyVar(..), TyVar(..) )
-import TcType ( TcType(..), TcMaybe(..), TcTauType(..), TcTyVar(..),
- tcReadTyVar, tcWriteTyVar
+import Type ( GenType(..), typeKind, mkFunTy, getFunTy_maybe )
+import TyCon ( TyCon, mkFunTyCon )
+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:
-import Kind ( Kind, isSubKindOf )
+import Kind ( Kind, hasMoreBoxityInfo, mkTypeKind )
+import Usage ( duffUsage )
import PprType ( GenTyVar, GenType ) -- instances
import Pretty
import Unique ( Unique ) -- instances
import Util
+
+#if __GLASGOW_HASKELL__ >= 202
+import Outputable
+#endif
+
\end{code}
\begin{code}
unifyTauTy :: TcTauType s -> TcTauType s -> TcM s ()
-unifyTauTy ty1 ty2
- = tcAddErrCtxt (unifyCtxt ty1 ty2) $
+unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred
+ = tcAddErrCtxtM (unifyCtxt ty1 ty2) $
uTys ty1 ty1 ty2 ty2
\end{code}
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
-- 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 fun1 arg1) _ (AppTy 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
+
+ -- Special case: converts a -> b to (->) a b
+uTys _ (AppTy s1 t1) _ (FunTy fun2 arg2 _)
+ = uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
+ where
+ s2 = AppTy (TyConTy mkFunTyCon duffUsage) fun2
+ t2 = arg2
+
+uTys _ (FunTy fun1 arg1 _) _ (AppTy s2 t2)
+ = uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
+ where
+ s1 = AppTy (TyConTy mkFunTyCon duffUsage) fun1
+ t1 = arg1
-- Type constructors must match
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
- -- Special case: converts (->) a b to a -> b
-uTys ps_ty1 (AppTy (AppTy (TyConTy FunTyCon u) fun) arg) ps_ty2 ty2
- = uTys ps_ty1 (FunTy fun arg u) ps_ty2 ty2
-uTys ps_ty1 ty1 ps_ty2 (AppTy (AppTy (TyConTy FunTyCon u) fun) arg)
- = uTys ps_ty1 ty1 ps_ty2 (FunTy fun arg u)
+ -- 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}
+Notes on synonyms
+~~~~~~~~~~~~~~~~~
+If you are tempted to make a short cut on synonyms, as in this
+pseudocode...
+
+\begin{verbatim}
+uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
+ = if (con1 == con2) then
+ -- Good news! Same synonym constructors, so we can shortcut
+ -- by unifying their arguments and ignoring their expansions.
+ unifyTauTypeLists args1 args2
+ else
+ -- Never mind. Just expand them and try again
+ uTys ty1 ty2
+\end{verbatim}
+
+then THINK AGAIN. Here is the whole story, as detected and reported
+by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
+\begin{quotation}
+Here's a test program that should detect the problem:
+
+\begin{verbatim}
+ type Bogus a = Int
+ x = (1 :: Bogus Char) :: Bogus Bool
+\end{verbatim}
+
+The problem with [the attempted shortcut code] is that
+\begin{verbatim}
+ con1 == con2
+\end{verbatim}
+is not a sufficient condition to be able to use the shortcut!
+You also need to know that the type synonym actually USES all
+its arguments. For example, consider the following type synonym
+which does not use all its arguments.
+\begin{verbatim}
+ type Bogus a = Int
+\end{verbatim}
+
+If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
+the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
+would fail, even though the expanded forms (both \tr{Int}) should
+match.
+
+Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
+unnecessarily bind \tr{t} to \tr{Char}.
+
+... You could explicitly test for the problem synonyms and mark them
+somehow as needing expansion, perhaps also issuing a warning to the
+user.
+\end{quotation}
+
+
%************************************************************************
%* *
\subsection[Unify-uVar]{@uVar@: unifying with a type variable}
= tcReadTyVar tv1 `thenNF_Tc` \ maybe_ty1 ->
case maybe_ty1 of
BoundTo ty1 -> uTys ty1 ty1 ps_ty2 ty2
- UnBound -> uUnboundVar tv1 ps_ty2 ty2
+ other -> uUnboundVar tv1 maybe_ty1 ps_ty2 ty2
-- Expand synonyms
-uUnboundVar tv1 ps_ty2 (SynTy _ _ ty2) = uUnboundVar tv1 ps_ty2 ty2
+uUnboundVar tv1 maybe_ty1 ps_ty2 (SynTy _ _ ty2)
+ = uUnboundVar tv1 maybe_ty1 ps_ty2 ty2
-- The both-type-variable case
uUnboundVar tv1@(TyVar uniq1 kind1 name1 box1)
+ maybe_ty1
ps_ty2
ty2@(TyVarTy tv2@(TyVar uniq2 kind2 name2 box2))
= returnTc ()
-- Distinct type variables
+ -- ASSERT maybe_ty1 /= BoundTo
| otherwise
= tcReadTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
- case maybe_ty2 of
- BoundTo ty2' -> uUnboundVar tv1 ty2' ty2'
- UnBound -> if kind2 `isSubKindOf` kind1 then
- tcWriteTyVar tv1 ty2 `thenNF_Tc_` returnTc ()
- else if kind1 `isSubKindOf` kind2 then
- tcWriteTyVar tv2 (TyVarTy tv1) `thenNF_Tc_` returnTc ()
- else
- failTc (unifyKindErr tv1 ps_ty2)
+ case (maybe_ty1, maybe_ty2) of
+ (_, BoundTo ty2') -> uUnboundVar tv1 maybe_ty1 ty2' ty2'
+
+ (UnBound, _) | kind2 `hasMoreBoxityInfo` kind1
+ -> tcWriteTyVar tv1 ps_ty2 `thenNF_Tc_` returnTc ()
+
+ (_, UnBound) | kind1 `hasMoreBoxityInfo` kind2
+ -> tcWriteTyVar tv2 (TyVarTy tv1) `thenNF_Tc_` returnTc ()
+
+-- TEMPORARY FIX
+-- (DontBind,DontBind)
+-- -> failTc (unifyDontBindErr tv1 ps_ty2)
+
+-- TEMPORARILY allow two type-sig variables to be bound together.
+-- See notes in tcCheckSigVars
+ (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
-uUnboundVar tv1@(TyVar uniq1 kind1 name1 box1) ps_ty2 non_var_ty2
- = occur_check non_var_ty2 `thenTc_`
- checkTc (getTypeKind non_var_ty2 `isSubKindOf` kind1)
- (unifyKindErr tv1 ps_ty2) `thenTc_`
- tcWriteTyVar tv1 non_var_ty2 `thenNF_Tc_`
- returnTc ()
+uUnboundVar tv1@(TyVar uniq1 kind1 name1 box1) maybe_ty1 ps_ty2 non_var_ty2
+ = case maybe_ty1 of
+ DontBind -> failTc (unifyDontBindErr tv1 ps_ty2)
+
+ UnBound | typeKind non_var_ty2 `hasMoreBoxityInfo` kind1
+ -> occur_check non_var_ty2 `thenTc_`
+ tcWriteTyVar tv1 ps_ty2 `thenNF_Tc_`
+ returnTc ()
+
+ other -> failTc (unifyKindErr tv1 ps_ty2)
where
occur_check (TyVarTy tv2@(TyVar uniq2 _ _ box2))
| uniq1 == uniq2 -- Same tyvar; fail
= tcReadTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
case maybe_ty2 of
BoundTo ty2' -> occur_check ty2'
- UnBound -> returnTc ()
+ other -> returnTc ()
occur_check (AppTy fun arg) = occur_check fun `thenTc_` occur_check arg
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}
-Notes on synonyms
-~~~~~~~~~~~~~~~~~
-If you are tempted to make a short cut on synonyms, as in this
-pseudocode...
+%************************************************************************
+%* *
+\subsection[Unify-fun]{@unifyFunTy@}
+%* *
+%************************************************************************
-\begin{verbatim}
-uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
- = if (con1 == con2) then
- -- Good news! Same synonym constructors, so we can shortcut
- -- by unifying their arguments and ignoring their expansions.
- unifyTauTypeLists args1 args2
- else
- -- Never mind. Just expand them and try again
- uTys ty1 ty2
-\end{verbatim}
+@unifyFunTy@ is used to avoid the fruitless creation of type variables.
-then THINK AGAIN. Here is the whole story, as detected and reported
-by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
-\begin{quotation}
-Here's a test program that should detect the problem:
+\begin{code}
+unifyFunTy :: TcType s -- Fail if ty isn't a function type
+ -> TcM s (TcType s, TcType s) -- otherwise return arg and result types
-\begin{verbatim}
- type Bogus a = Int
- x = (1 :: Bogus Char) :: Bogus Bool
-\end{verbatim}
+unifyFunTy ty@(TyVarTy tyvar)
+ = tcReadTyVar tyvar `thenNF_Tc` \ maybe_ty ->
+ case maybe_ty of
+ BoundTo ty' -> unifyFunTy ty'
-The problem with [the attempted shortcut code] is that
-\begin{verbatim}
- con1 == con2
-\end{verbatim}
-is not a sufficient condition to be able to use the shortcut!
-You also need to know that the type synonym actually USES all
-its arguments. For example, consider the following type synonym
-which does not use all its arguments.
-\begin{verbatim}
- type Bogus a = Int
-\end{verbatim}
+ UnBound -> newTyVarTy mkTypeKind `thenNF_Tc` \ arg ->
+ newTyVarTy mkTypeKind `thenNF_Tc` \ res ->
+ tcWriteTyVar tyvar (mkFunTy arg res) `thenNF_Tc_`
+ returnTc (arg,res)
-If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
-the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
-would fail, even though the expanded forms (both \tr{Int}) should
-match.
+ DontBind -> failTc (expectedFunErr ty)
-Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
-unnecessarily bind \tr{t} to \tr{Char}.
+unifyFunTy other_ty
+ = case getFunTy_maybe other_ty of
+ Just arg_and_res -> returnTc arg_and_res
+ Nothing -> failTc (expectedFunErr other_ty)
+\end{code}
-... You could explicitly test for the problem synonyms and mark them
-somehow as needing expansion, perhaps also issuing a warning to the
-user.
-\end{quotation}
+%************************************************************************
+%* *
+\subsection[Unify-context]{Errors and contexts}
+%* *
+%************************************************************************
Errors
~~~~~~
\begin{code}
-unifyCtxt ty1 ty2 sty
- = ppAboves [
- ppCat [ppStr "Expected:", ppr sty ty1],
- ppCat [ppStr " Actual:", ppr sty 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 = 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
+ = hang (text "Function type expected, but found the type")
+ 4 (ppr sty ty)
unifyKindErr tyvar ty sty
- = ppHang (ppStr "Kind mis-match between")
- 4 (ppSep [ppr sty tyvar, ppStr "and", ppr sty ty])
+ = 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
+ = 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 "Occur check: cannot construct the infinite type")
- 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}
projects / ghc-hetmet.git / blobdiff