[project @ 2000-07-14 13:37:53 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcUnify.lhs
1 %
2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
3 %
4 \section[Unify]{Unifier}
5
6 The unifier is now squarely in the typechecker monad (because of the
7 updatable substitution).
8
9 \begin{code}
10 module TcUnify ( unifyTauTy, unifyTauTyList, unifyTauTyLists, 
11                  unifyFunTy, unifyListTy, unifyTupleTy,
12                  unifyKind, unifyKinds, unifyOpenTypeKind
13  ) where
14
15 #include "HsVersions.h"
16
17 -- friends: 
18 import TcMonad
19 import TypeRep  ( Type(..) )  -- friend
20 import Type     ( funTyCon, Kind, unboxedTypeKind, boxedTypeKind, openTypeKind, 
21                   superBoxity, typeCon, openKindCon, hasMoreBoxityInfo, 
22                   tyVarsOfType, typeKind,
23                   mkTyVarTy, mkFunTy, splitFunTy_maybe, splitTyConApp_maybe,
24                   isNotUsgTy, splitAppTy_maybe, mkTyConApp, 
25                   tidyOpenType, tidyOpenTypes, tidyTyVar
26                 )
27 import TyCon    ( TyCon, isTupleTyCon, tupleTyConBoxity, tyConArity )
28 import Name     ( hasBetterProv )
29 import Var      ( TyVar, tyVarKind, varName, isSigTyVar )
30 import VarSet   ( varSetElems )
31 import TcType   ( TcType, TcTauType, TcTyVar, TcKind, newBoxityVar,
32                   newTyVarTy, newTyVarTys, tcGetTyVar, tcPutTyVar, zonkTcType
33                 )
34
35 -- others:
36 import BasicTypes ( Arity, Boxity, isBoxed )
37 import TysWiredIn ( listTyCon, mkListTy, mkTupleTy )
38 import Outputable
39 \end{code}
40
41
42 %************************************************************************
43 %*                                                                      *
44 \subsection{The Kind variants}
45 %*                                                                      *
46 %************************************************************************
47
48 \begin{code}
49 unifyKind :: TcKind                 -- Expected
50           -> TcKind                 -- Actual
51           -> TcM s ()
52 unifyKind k1 k2 
53   = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $
54     uTys k1 k1 k2 k2
55
56 unifyKinds :: [TcKind] -> [TcKind] -> TcM s ()
57 unifyKinds []       []       = returnTc ()
58 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2  `thenTc_`
59                                unifyKinds ks1 ks2
60 unifyKinds _ _ = panic "unifyKinds: length mis-match"
61 \end{code}
62
63 \begin{code}
64 unifyOpenTypeKind :: TcKind -> TcM s () 
65 -- Ensures that the argument kind is of the form (Type bx)
66 -- for some boxity bx
67
68 unifyOpenTypeKind ty@(TyVarTy tyvar)
69   = tcGetTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
70     case maybe_ty of
71         Just ty' -> unifyOpenTypeKind ty'
72         other    -> unify_open_kind_help ty
73
74 unifyOpenTypeKind ty
75   = case splitTyConApp_maybe ty of
76         Just (tycon, [_]) | tycon == typeCon -> returnTc ()
77         other                                -> unify_open_kind_help ty
78
79 unify_open_kind_help ty -- Revert to ordinary unification
80   = newBoxityVar        `thenNF_Tc` \ boxity ->
81     unifyKind ty (mkTyConApp typeCon [boxity])
82 \end{code}
83
84
85 %************************************************************************
86 %*                                                                      *
87 \subsection[Unify-exported]{Exported unification functions}
88 %*                                                                      *
89 %************************************************************************
90
91 The exported functions are all defined as versions of some
92 non-exported generic functions.
93
94 Unify two @TauType@s.  Dead straightforward.
95
96 \begin{code}
97 unifyTauTy :: TcTauType -> TcTauType -> TcM s ()
98 unifyTauTy ty1 ty2      -- ty1 expected, ty2 inferred
99   = tcAddErrCtxtM (unifyCtxt "type" ty1 ty2) $
100     uTys ty1 ty1 ty2 ty2
101 \end{code}
102
103 @unifyTauTyList@ unifies corresponding elements of two lists of
104 @TauType@s.  It uses @uTys@ to do the real work.  The lists should be
105 of equal length.  We charge down the list explicitly so that we can
106 complain if their lengths differ.
107
108 \begin{code}
109 unifyTauTyLists :: [TcTauType] -> [TcTauType] ->  TcM s ()
110 unifyTauTyLists []           []         = returnTc ()
111 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2   `thenTc_`
112                                         unifyTauTyLists tys1 tys2
113 unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
114 \end{code}
115
116 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
117 all together.  It is used, for example, when typechecking explicit
118 lists, when all the elts should be of the same type.
119
120 \begin{code}
121 unifyTauTyList :: [TcTauType] -> TcM s ()
122 unifyTauTyList []                = returnTc ()
123 unifyTauTyList [ty]              = returnTc ()
124 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2   `thenTc_`
125                                    unifyTauTyList tys
126 \end{code}
127
128 %************************************************************************
129 %*                                                                      *
130 \subsection[Unify-uTys]{@uTys@: getting down to business}
131 %*                                                                      *
132 %************************************************************************
133
134 @uTys@ is the heart of the unifier.  Each arg happens twice, because
135 we want to report errors in terms of synomyms if poss.  The first of
136 the pair is used in error messages only; it is always the same as the
137 second, except that if the first is a synonym then the second may be a
138 de-synonym'd version.  This way we get better error messages.
139
140 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
141
142 \begin{code}
143 uTys :: TcTauType -> TcTauType  -- Error reporting ty1 and real ty1
144                                 -- ty1 is the *expected* type
145
146      -> TcTauType -> TcTauType  -- Error reporting ty2 and real ty2
147                                 -- ty2 is the *actual* type
148      -> TcM s ()
149
150         -- Always expand synonyms (see notes at end)
151         -- (this also throws away FTVs and usage annots)
152 uTys ps_ty1 (NoteTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
153 uTys ps_ty1 ty1 ps_ty2 (NoteTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
154
155         -- Variables; go for uVar
156 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
157 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True  tyvar2 ps_ty1 ty1
158                                         -- "True" means args swapped
159
160         -- Functions; just check the two parts
161 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
162   = uTys fun1 fun1 fun2 fun2    `thenTc_`    uTys arg1 arg1 arg2 arg2
163
164         -- Type constructors must match
165 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
166   | con1 == con2 && length tys1 == length tys2
167   = unifyTauTyLists tys1 tys2
168
169   | con1 == openKindCon
170         -- When we are doing kind checking, we might match a kind '?' 
171         -- against a kind '*' or '#'.  Notably, CCallable :: ? -> *, and
172         -- (CCallable Int) and (CCallable Int#) are both OK
173   = unifyOpenTypeKind ps_ty2
174
175   | otherwise
176   = unifyMisMatch ps_ty1 ps_ty2
177
178
179         -- Applications need a bit of care!
180         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
181         -- NB: we've already dealt with type variables and Notes,
182         -- so if one type is an App the other one jolly well better be too
183 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
184   = case splitAppTy_maybe ty2 of
185         Just (s2,t2) -> uTys s1 s1 s2 s2        `thenTc_`    uTys t1 t1 t2 t2
186         Nothing      -> unifyMisMatch ps_ty1 ps_ty2
187
188         -- Now the same, but the other way round
189         -- Don't swap the types, because the error messages get worse
190 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
191   = case splitAppTy_maybe ty1 of
192         Just (s1,t1) -> uTys s1 s1 s2 s2        `thenTc_`    uTys t1 t1 t2 t2
193         Nothing      -> unifyMisMatch ps_ty1 ps_ty2
194
195         -- Not expecting for-alls in unification
196         -- ... but the error message from the unifyMisMatch more informative
197         -- than a panic message!
198
199         -- Anything else fails
200 uTys ps_ty1 ty1 ps_ty2 ty2  = unifyMisMatch ps_ty1 ps_ty2
201 \end{code}
202
203 Notes on synonyms
204 ~~~~~~~~~~~~~~~~~
205 If you are tempted to make a short cut on synonyms, as in this
206 pseudocode...
207
208 \begin{verbatim}
209 uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
210   = if (con1 == con2) then
211         -- Good news!  Same synonym constructors, so we can shortcut
212         -- by unifying their arguments and ignoring their expansions.
213         unifyTauTypeLists args1 args2
214     else
215         -- Never mind.  Just expand them and try again
216         uTys ty1 ty2
217 \end{verbatim}
218
219 then THINK AGAIN.  Here is the whole story, as detected and reported
220 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
221 \begin{quotation}
222 Here's a test program that should detect the problem:
223
224 \begin{verbatim}
225         type Bogus a = Int
226         x = (1 :: Bogus Char) :: Bogus Bool
227 \end{verbatim}
228
229 The problem with [the attempted shortcut code] is that
230 \begin{verbatim}
231         con1 == con2
232 \end{verbatim}
233 is not a sufficient condition to be able to use the shortcut!
234 You also need to know that the type synonym actually USES all
235 its arguments.  For example, consider the following type synonym
236 which does not use all its arguments.
237 \begin{verbatim}
238         type Bogus a = Int
239 \end{verbatim}
240
241 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
242 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
243 would fail, even though the expanded forms (both \tr{Int}) should
244 match.
245
246 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
247 unnecessarily bind \tr{t} to \tr{Char}.
248
249 ... You could explicitly test for the problem synonyms and mark them
250 somehow as needing expansion, perhaps also issuing a warning to the
251 user.
252 \end{quotation}
253
254
255 %************************************************************************
256 %*                                                                      *
257 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
258 %*                                                                      *
259 %************************************************************************
260
261 @uVar@ is called when at least one of the types being unified is a
262 variable.  It does {\em not} assume that the variable is a fixed point
263 of the substitution; rather, notice that @uVar@ (defined below) nips
264 back into @uTys@ if it turns out that the variable is already bound.
265
266 \begin{code}
267 uVar :: Bool            -- False => tyvar is the "expected"
268                         -- True  => ty    is the "expected" thing
269      -> TcTyVar
270      -> TcTauType -> TcTauType  -- printing and real versions
271      -> TcM s ()
272
273 uVar swapped tv1 ps_ty2 ty2
274   = tcGetTyVar tv1      `thenNF_Tc` \ maybe_ty1 ->
275     case maybe_ty1 of
276         Just ty1 | swapped   -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
277                  | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
278         other       -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
279
280         -- Expand synonyms; ignore FTVs; ignore usage annots
281 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy _ ty2)
282   = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
283
284
285         -- The both-type-variable case
286 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
287
288         -- Same type variable => no-op
289   | tv1 == tv2
290   = returnTc ()
291
292         -- Distinct type variables
293         -- ASSERT maybe_ty1 /= Just
294   | otherwise
295   = tcGetTyVar tv2      `thenNF_Tc` \ maybe_ty2 ->
296     case maybe_ty2 of
297         Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
298
299         Nothing | tv1_dominates_tv2 
300
301                 -> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
302                    tcPutTyVar tv2 (TyVarTy tv1)         `thenNF_Tc_`
303                    returnTc ()
304                 |  otherwise
305
306                 -> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
307                    (ASSERT( isNotUsgTy ps_ty2 )
308                     tcPutTyVar tv1 ps_ty2               `thenNF_Tc_`
309                     returnTc ())
310   where
311     k1 = tyVarKind tv1
312     k2 = tyVarKind tv2
313     tv1_dominates_tv2 =    isSigTyVar tv1 
314                                 -- Don't unify a signature type variable if poss
315                         || k2 == openTypeKind
316                                 -- Try to get rid of open type variables as soon as poss
317                         || varName tv1 `hasBetterProv` varName tv2 
318                                 -- Try to update sys-y type variables in preference to sig-y ones
319
320         -- Second one isn't a type variable
321 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
322   = checkKinds swapped tv1 non_var_ty2                  `thenTc_`
323     occur_check non_var_ty2                             `thenTc_`
324     ASSERT( isNotUsgTy ps_ty2 )
325     checkTcM (not (isSigTyVar tv1))
326              (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_`
327
328     warnTc (not (typeKind non_var_ty2 `hasMoreBoxityInfo` tyVarKind tv1))
329            ((ppr tv1 <+> ppr (tyVarKind tv1)) $$ 
330              (ppr non_var_ty2 <+> ppr (typeKind non_var_ty2)))          `thenNF_Tc_` 
331
332     tcPutTyVar tv1 non_var_ty2                          `thenNF_Tc_`
333         -- This used to say "ps_ty2" instead of "non_var_ty2"
334
335         -- But that led to an infinite loop in the type checker!
336         -- Consider 
337         --      type A a = ()
338         --
339         --      f :: (A a -> a -> ()) -> ()
340         --      f = \ _ -> ()
341         --
342         --      x :: ()
343         --      x = f (\ x p -> p x)
344         --
345         -- Here, we try to match "t" with "A t", and succeed
346         -- because the unifier looks through synonyms.  The occurs
347         -- check doesn't kick in because we are "really" binding "t" to "()",
348         -- but we *actually* bind "t" to "A t" if we store ps_ty2.
349         -- That leads the typechecker into an infinite loop later.
350
351     returnTc ()
352   where
353     occur_check ty = mapTc occur_check_tv (varSetElems (tyVarsOfType ty))       `thenTc_`
354                      returnTc ()
355
356     occur_check_tv tv2
357        | tv1 == tv2             -- Same tyvar; fail
358        = zonkTcType ps_ty2      `thenNF_Tc` \ zonked_ty2 ->
359          failWithTcM (unifyOccurCheck tv1 zonked_ty2)
360
361        | otherwise              -- A different tyvar
362        = tcGetTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
363          case maybe_ty2 of
364                 Just ty2' -> occur_check ty2'
365                 other     -> returnTc ()
366
367 checkKinds swapped tv1 ty2
368 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
369 -- We need to check that we don't unify a boxed type variable with an
370 -- unboxed type: e.g.  (id 3#) is illegal
371   | tk1 == boxedTypeKind && tk2 == unboxedTypeKind
372   = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2)       $
373     unifyMisMatch k1 k2
374   | otherwise
375   = returnTc ()
376   where
377     (k1,k2) | swapped   = (tk2,tk1)
378             | otherwise = (tk1,tk2)
379     tk1 = tyVarKind tv1
380     tk2 = typeKind ty2
381 \end{code}
382
383
384 %************************************************************************
385 %*                                                                      *
386 \subsection[Unify-fun]{@unifyFunTy@}
387 %*                                                                      *
388 %************************************************************************
389
390 @unifyFunTy@ is used to avoid the fruitless creation of type variables.
391
392 \begin{code}
393 unifyFunTy :: TcType                            -- Fail if ty isn't a function type
394            -> TcM s (TcType, TcType)    -- otherwise return arg and result types
395
396 unifyFunTy ty@(TyVarTy tyvar)
397   = tcGetTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
398     case maybe_ty of
399         Just ty' -> unifyFunTy ty'
400         other       -> unify_fun_ty_help ty
401
402 unifyFunTy ty
403   = case splitFunTy_maybe ty of
404         Just arg_and_res -> returnTc arg_and_res
405         Nothing          -> unify_fun_ty_help ty
406
407 unify_fun_ty_help ty    -- Special cases failed, so revert to ordinary unification
408   = newTyVarTy openTypeKind     `thenNF_Tc` \ arg ->
409     newTyVarTy openTypeKind     `thenNF_Tc` \ res ->
410     unifyTauTy ty (mkFunTy arg res)     `thenTc_`
411     returnTc (arg,res)
412 \end{code}
413
414 \begin{code}
415 unifyListTy :: TcType              -- expected list type
416             -> TcM s TcType      -- list element type
417
418 unifyListTy ty@(TyVarTy tyvar)
419   = tcGetTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
420     case maybe_ty of
421         Just ty' -> unifyListTy ty'
422         other       -> unify_list_ty_help ty
423
424 unifyListTy ty
425   = case splitTyConApp_maybe ty of
426         Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
427         other                                       -> unify_list_ty_help ty
428
429 unify_list_ty_help ty   -- Revert to ordinary unification
430   = newTyVarTy boxedTypeKind            `thenNF_Tc` \ elt_ty ->
431     unifyTauTy ty (mkListTy elt_ty)     `thenTc_`
432     returnTc elt_ty
433 \end{code}
434
435 \begin{code}
436 unifyTupleTy :: Boxity -> Arity -> TcType -> TcM s [TcType]
437 unifyTupleTy boxity arity ty@(TyVarTy tyvar)
438   = tcGetTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
439     case maybe_ty of
440         Just ty' -> unifyTupleTy boxity arity ty'
441         other    -> unify_tuple_ty_help boxity arity ty
442
443 unifyTupleTy boxity arity ty
444   = case splitTyConApp_maybe ty of
445         Just (tycon, arg_tys)
446                 |  isTupleTyCon tycon 
447                 && tyConArity tycon == arity
448                 && tupleTyConBoxity tycon == boxity
449                 -> returnTc arg_tys
450         other -> unify_tuple_ty_help boxity arity ty
451
452 unify_tuple_ty_help boxity arity ty
453   = newTyVarTys arity kind                              `thenNF_Tc` \ arg_tys ->
454     unifyTauTy ty (mkTupleTy boxity arity arg_tys)      `thenTc_`
455     returnTc arg_tys
456   where
457     kind | isBoxed boxity = boxedTypeKind
458          | otherwise      = openTypeKind
459 \end{code}
460
461
462 %************************************************************************
463 %*                                                                      *
464 \subsection[Unify-context]{Errors and contexts}
465 %*                                                                      *
466 %************************************************************************
467
468 Errors
469 ~~~~~~
470
471 \begin{code}
472 unifyCtxt s ty1 ty2 tidy_env    -- ty1 expected, ty2 inferred
473   = zonkTcType ty1      `thenNF_Tc` \ ty1' ->
474     zonkTcType ty2      `thenNF_Tc` \ ty2' ->
475     returnNF_Tc (err ty1' ty2')
476   where
477     err ty1 ty2 = (env1, 
478                    nest 4 
479                         (vcat [
480                            text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
481                            text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
482                         ]))
483                   where
484                     (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
485
486 unifyKindCtxt swapped tv1 ty2 tidy_env  -- not swapped => tv1 expected, ty2 inferred
487         -- tv1 is zonked already
488   = zonkTcType ty2      `thenNF_Tc` \ ty2' ->
489     returnNF_Tc (err ty2')
490   where
491     err ty2 = (env2, ptext SLIT("When matching types") <+> 
492                      sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
493             where
494               (pp_expected, pp_actual) | swapped   = (pp2, pp1)
495                                        | otherwise = (pp1, pp2)
496               (env1, tv1') = tidyTyVar tidy_env tv1
497               (env2, ty2') = tidyOpenType  env1 ty2
498               pp1 = ppr tv1'
499               pp2 = ppr ty2'
500
501 unifyMisMatch ty1 ty2
502   = zonkTcType ty1      `thenNF_Tc` \ ty1' ->
503     zonkTcType ty2      `thenNF_Tc` \ ty2' ->
504     let
505         (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
506         msg = hang (ptext SLIT("Couldn't match"))
507                    4 (sep [quotes (ppr tidy_ty1), 
508                            ptext SLIT("against"), 
509                            quotes (ppr tidy_ty2)])
510     in
511     failWithTcM (env, msg)
512
513 unifyWithSigErr tyvar ty
514   = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
515               4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
516   where
517     (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
518     (env2, tidy_ty)    = tidyOpenType  env1     ty
519
520 unifyOccurCheck tyvar ty
521   = (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
522               4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
523   where
524     (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
525     (env2, tidy_ty)    = tidyOpenType  env1     ty
526 \end{code}
527