2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1996
4 \section[Unify]{Unifier}
6 The unifier is now squarely in the typechecker monad (because of the
7 updatable substitution).
10 #include "HsVersions.h"
12 module Unify ( unifyTauTy, unifyTauTyList, unifyTauTyLists, unifyFunTy ) where
18 import Type ( GenType(..), typeKind, mkFunTy, getFunTy_maybe )
19 import TyCon ( TyCon, mkFunTyCon )
20 import TyVar ( GenTyVar(..), SYN_IE(TyVar), tyVarKind )
21 import TcType ( SYN_IE(TcType), TcMaybe(..), SYN_IE(TcTauType), SYN_IE(TcTyVar),
22 newTyVarTy, tcReadTyVar, tcWriteTyVar, zonkTcType
25 import Kind ( Kind, hasMoreBoxityInfo, mkTypeKind )
26 import Usage ( duffUsage )
27 import PprType ( GenTyVar, GenType ) -- instances
29 import Unique ( Unique ) -- instances
34 %************************************************************************
36 \subsection[Unify-exported]{Exported unification functions}
38 %************************************************************************
40 The exported functions are all defined as versions of some
41 non-exported generic functions.
43 Unify two @TauType@s. Dead straightforward.
46 unifyTauTy :: TcTauType s -> TcTauType s -> TcM s ()
47 unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred
48 = tcAddErrCtxtM (unifyCtxt ty1 ty2) $
52 @unifyTauTyList@ unifies corresponding elements of two lists of
53 @TauType@s. It uses @uTys@ to do the real work. The lists should be
54 of equal length. We charge down the list explicitly so that we can
55 complain if their lengths differ.
58 unifyTauTyLists :: [TcTauType s] -> [TcTauType s] -> TcM s ()
59 unifyTauTyLists [] [] = returnTc ()
60 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenTc_`
61 unifyTauTyLists tys1 tys2
62 unifyTauTypeLists ty1s ty2s = panic "Unify.unifyTauTypeLists: mismatched type lists!"
65 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
66 all together. It is used, for example, when typechecking explicit
67 lists, when all the elts should be of the same type.
70 unifyTauTyList :: [TcTauType s] -> TcM s ()
71 unifyTauTyList [] = returnTc ()
72 unifyTauTyList [ty] = returnTc ()
73 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenTc_`
77 %************************************************************************
79 \subsection[Unify-uTys]{@uTys@: getting down to business}
81 %************************************************************************
83 @uTys@ is the heart of the unifier. Each arg happens twice, because
84 we want to report errors in terms of synomyms if poss. The first of
85 the pair is used in error messages only; it is always the same as the
86 second, except that if the first is a synonym then the second may be a
87 de-synonym'd version. This way we get better error messages.
89 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
92 uTys :: TcTauType s -> TcTauType s -- Error reporting ty1 and real ty1
93 -> TcTauType s -> TcTauType s -- Error reporting ty2 and real ty2
96 -- Variables; go for uVar
97 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar tyvar1 ps_ty2 ty2
98 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar tyvar2 ps_ty1 ty1
100 -- Applications and functions; just check the two parts
101 uTys _ (FunTy fun1 arg1 _) _ (FunTy fun2 arg2 _)
102 = uTys fun1 fun1 fun2 fun2 `thenTc_` uTys arg1 arg1 arg2 arg2
103 uTys _ (AppTy s1 t1) _ (AppTy s2 t2)
104 = uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
106 -- Special case: converts a -> b to (->) a b
107 uTys _ (AppTy s1 t1) _ (FunTy fun2 arg2 _)
108 = uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
110 s2 = AppTy (TyConTy mkFunTyCon duffUsage) fun2
113 uTys _ (FunTy fun1 arg1 _) _ (AppTy s2 t2)
114 = uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
116 s1 = AppTy (TyConTy mkFunTyCon duffUsage) fun1
119 -- Type constructors must match
120 uTys ps_ty1 (TyConTy con1 _) ps_ty2 (TyConTy con2 _)
121 = checkTc (con1 == con2) (unifyMisMatch ps_ty1 ps_ty2)
123 -- Always expand synonyms (see notes at end)
124 uTys ps_ty1 (SynTy con1 args1 ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
125 uTys ps_ty1 ty1 ps_ty2 (SynTy con2 args2 ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
127 -- Not expecting for-alls in unification
129 uTys ps_ty1 (ForAllTy _ _) ps_ty2 ty2 = panic "Unify.uTys:ForAllTy (1st arg)"
130 uTys ps_ty1 ty1 ps_ty2 (ForAllTy _ _) = panic "Unify.uTys:ForAllTy (2nd arg)"
131 uTys ps_ty1 (ForAllUsageTy _ _ _) ps_ty2 ty2 = panic "Unify.uTys:ForAllUsageTy (1st arg)"
132 uTys ps_ty1 ty1 ps_ty2 (ForAllUsageTy _ _ _) = panic "Unify.uTys:ForAllUsageTy (2nd arg)"
135 -- Anything else fails
136 uTys ps_ty1 ty1 ps_ty2 ty2 = failTc (unifyMisMatch ps_ty1 ps_ty2)
141 If you are tempted to make a short cut on synonyms, as in this
145 uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
146 = if (con1 == con2) then
147 -- Good news! Same synonym constructors, so we can shortcut
148 -- by unifying their arguments and ignoring their expansions.
149 unifyTauTypeLists args1 args2
151 -- Never mind. Just expand them and try again
155 then THINK AGAIN. Here is the whole story, as detected and reported
156 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
158 Here's a test program that should detect the problem:
162 x = (1 :: Bogus Char) :: Bogus Bool
165 The problem with [the attempted shortcut code] is that
169 is not a sufficient condition to be able to use the shortcut!
170 You also need to know that the type synonym actually USES all
171 its arguments. For example, consider the following type synonym
172 which does not use all its arguments.
177 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
178 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
179 would fail, even though the expanded forms (both \tr{Int}) should
182 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
183 unnecessarily bind \tr{t} to \tr{Char}.
185 ... You could explicitly test for the problem synonyms and mark them
186 somehow as needing expansion, perhaps also issuing a warning to the
191 %************************************************************************
193 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
195 %************************************************************************
197 @uVar@ is called when at least one of the types being unified is a
198 variable. It does {\em not} assume that the variable is a fixed point
199 of the substitution; rather, notice that @bindTo@ (defined below) nips
200 back into @uTys@ if it turns out that the variable is already bound.
202 There is a slight worry that one might try to @bindTo@ a (say) Poly
203 tyvar (as tv1) with an Open tyvar (as ty2) which is already unified to
204 an unboxed type. In fact this can't happen, because the Open ones are
205 always the ones which are unified away.
209 -> TcTauType s -> TcTauType s -- printing and real versions
213 = tcReadTyVar tv1 `thenNF_Tc` \ maybe_ty1 ->
215 BoundTo ty1 -> uTys ty1 ty1 ps_ty2 ty2
216 other -> uUnboundVar tv1 maybe_ty1 ps_ty2 ty2
219 uUnboundVar tv1 maybe_ty1 ps_ty2 (SynTy _ _ ty2)
220 = uUnboundVar tv1 maybe_ty1 ps_ty2 ty2
223 -- The both-type-variable case
224 uUnboundVar tv1@(TyVar uniq1 kind1 name1 box1)
227 ty2@(TyVarTy tv2@(TyVar uniq2 kind2 name2 box2))
229 -- Same type variable => no-op
233 -- Distinct type variables
234 -- ASSERT maybe_ty1 /= BoundTo
236 = tcReadTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
237 case (maybe_ty1, maybe_ty2) of
238 (_, BoundTo ty2') -> uUnboundVar tv1 maybe_ty1 ty2' ty2'
240 (UnBound, _) | kind2 `hasMoreBoxityInfo` kind1
241 -> tcWriteTyVar tv1 ty2 `thenNF_Tc_` returnTc ()
243 (_, UnBound) | kind1 `hasMoreBoxityInfo` kind2
244 -> tcWriteTyVar tv2 (TyVarTy tv1) `thenNF_Tc_` returnTc ()
247 -- (DontBind,DontBind)
248 -- -> failTc (unifyDontBindErr tv1 ps_ty2)
250 -- TEMPORARILY allow two type-sig variables to be bound together.
251 -- See notes in tcCheckSigVars
252 (DontBind,DontBind) | kind2 `hasMoreBoxityInfo` kind1
253 -> tcWriteTyVar tv1 ty2 `thenNF_Tc_` returnTc ()
255 | kind1 `hasMoreBoxityInfo` kind2
256 -> tcWriteTyVar tv2 (TyVarTy tv1) `thenNF_Tc_` returnTc ()
258 other -> failTc (unifyKindErr tv1 ps_ty2)
260 -- Second one isn't a type variable
261 uUnboundVar tv1@(TyVar uniq1 kind1 name1 box1) maybe_ty1 ps_ty2 non_var_ty2
263 DontBind -> failTc (unifyDontBindErr tv1 ps_ty2)
265 UnBound | typeKind non_var_ty2 `hasMoreBoxityInfo` kind1
266 -> occur_check non_var_ty2 `thenTc_`
267 tcWriteTyVar tv1 ps_ty2 `thenNF_Tc_`
270 other -> failTc (unifyKindErr tv1 ps_ty2)
272 occur_check (TyVarTy tv2@(TyVar uniq2 _ _ box2))
273 | uniq1 == uniq2 -- Same tyvar; fail
274 = failTc (unifyOccurCheck tv1 ps_ty2)
276 | otherwise -- A different tyvar
277 = tcReadTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
279 BoundTo ty2' -> occur_check ty2'
282 occur_check (AppTy fun arg) = occur_check fun `thenTc_` occur_check arg
283 occur_check (FunTy fun arg _) = occur_check fun `thenTc_` occur_check arg
284 occur_check (TyConTy _ _) = returnTc ()
285 occur_check (SynTy _ _ ty2) = occur_check ty2
286 occur_check other = panic "Unexpected Dict or ForAll in occurCheck"
289 %************************************************************************
291 \subsection[Unify-fun]{@unifyFunTy@}
293 %************************************************************************
295 @unifyFunTy@ is used to avoid the fruitless creation of type variables.
298 unifyFunTy :: TcType s -- Fail if ty isn't a function type
299 -> TcM s (TcType s, TcType s) -- otherwise return arg and result types
301 unifyFunTy ty@(TyVarTy tyvar)
302 = tcReadTyVar tyvar `thenNF_Tc` \ maybe_ty ->
304 BoundTo ty' -> unifyFunTy ty'
306 UnBound -> newTyVarTy mkTypeKind `thenNF_Tc` \ arg ->
307 newTyVarTy mkTypeKind `thenNF_Tc` \ res ->
308 tcWriteTyVar tyvar (mkFunTy arg res) `thenNF_Tc_`
311 DontBind -> failTc (expectedFunErr ty)
314 = case getFunTy_maybe other_ty of
315 Just arg_and_res -> returnTc arg_and_res
316 Nothing -> failTc (expectedFunErr other_ty)
320 %************************************************************************
322 \subsection[Unify-context]{Errors and contexts}
324 %************************************************************************
330 unifyCtxt ty1 ty2 -- ty1 expected, ty2 inferred
331 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
332 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
333 returnNF_Tc (err ty1' ty2')
335 err ty1' ty2' sty = ppAboves [
336 ppCat [ppPStr SLIT("Expected:"), ppr sty ty1'],
337 ppCat [ppPStr SLIT("Inferred:"), ppr sty ty2']
340 unifyMisMatch ty1 ty2 sty
341 = ppHang (ppPStr SLIT("Couldn't match the type"))
342 4 (ppSep [ppr sty ty1, ppPStr SLIT("against"), ppr sty ty2])
344 expectedFunErr ty sty
345 = ppHang (ppStr "Function type expected, but found the type")
348 unifyKindErr tyvar ty sty
349 = ppHang (ppPStr SLIT("Compiler bug: kind mis-match between"))
350 4 (ppSep [ppCat [ppr sty tyvar, ppPStr SLIT("::"), ppr sty (tyVarKind tyvar)],
352 ppCat [ppr sty ty, ppPStr SLIT("::"), ppr sty (typeKind ty)]])
354 unifyDontBindErr tyvar ty sty
355 = ppHang (ppPStr SLIT("Couldn't match the signature/existential type variable"))
356 4 (ppSep [ppr sty tyvar,
357 ppPStr SLIT("with the type"),
360 unifyOccurCheck tyvar ty sty
361 = ppHang (ppPStr SLIT("Cannot construct the infinite type (occur check)"))
362 4 (ppSep [ppr sty tyvar, ppChar '=', ppr sty ty])