Fix GADT refinement fix-pointing, add ASSERTs and a WARN, make type equality function...
[ghc-hetmet.git] / compiler / typecheck / TcGadt.lhs
1 %
2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
3 %
4
5 %************************************************************************
6 %*                                                                      *
7                 Type refinement for GADTs
8 %*                                                                      *
9 %************************************************************************
10
11 \begin{code}
12 module TcGadt (
13         Refinement, emptyRefinement, gadtRefine, 
14         refineType, refineResType,
15         dataConCanMatch,
16         tcUnifyTys, BindFlag(..)
17   ) where
18
19 import HsSyn    ( ExprCoFn(..), idCoercion, isIdCoercion )
20 import Coercion ( Coercion, mkSymCoercion, mkTransCoercion, mkUnsafeCoercion,
21                   mkLeftCoercion, mkRightCoercion, mkCoKind, coercionKindPredTy,
22                   splitCoercionKind, decomposeCo )
23 import TcType   ( TvSubst(..), TvSubstEnv, substTy, mkTvSubst, 
24                   substTyVar, zipTopTvSubst, typeKind,
25                   eqKind, isSubKind, repSplitAppTy_maybe,
26                   tcView
27                 )
28 import Type     ( Type, tyVarsOfType, tyVarsOfTypes, tcEqType, mkTyVarTy )
29 import TypeRep  ( Type(..), PredType(..) )
30 import DataCon  ( DataCon, dataConUnivTyVars, dataConEqSpec )
31 import Var      ( CoVar, TyVar, tyVarKind )
32 import VarEnv
33 import VarSet
34 import ErrUtils         ( Message )
35 import Maybes           ( MaybeErr(..), isJust )
36 import Control.Monad    ( foldM )
37 import Outputable
38
39 #include "HsVersions.h"
40 \end{code}
41
42
43 %************************************************************************
44 %*                                                                      *
45                 What a refinement is
46 %*                                                                      *
47 %************************************************************************
48
49 \begin{code}
50 data Refinement = Reft InScopeSet InternalReft 
51 -- INVARIANT:   a->(co,ty)   then   co :: (a:=:ty)
52 -- Not necessarily idemopotent
53
54 instance Outputable Refinement where
55   ppr (Reft in_scope env)
56     = ptext SLIT("Refinement") <+>
57         braces (ppr env)
58
59 emptyRefinement :: Refinement
60 emptyRefinement = (Reft emptyInScopeSet emptyVarEnv)
61
62 refineType :: Refinement -> Type -> (ExprCoFn, Type)
63 -- Apply the refinement to the type.
64 -- If (refineType r ty) = (co, ty')
65 -- Then co :: ty:=:ty'
66 refineType (Reft in_scope env) ty
67   | not (isEmptyVarEnv env),            -- Common case
68     any (`elemVarEnv` env) (varSetElems (tyVarsOfType ty))
69   = (ExprCoFn (substTy co_subst ty), substTy tv_subst ty)
70   | otherwise
71   = (idCoercion, ty)    -- The type doesn't mention any refined type variables
72   where
73     tv_subst = mkTvSubst in_scope (mapVarEnv snd env)
74     co_subst = mkTvSubst in_scope (mapVarEnv fst env)
75  
76 refineResType :: Refinement -> Type -> (ExprCoFn, Type)
77 -- Like refineType, but returns the 'sym' coercion
78 -- If (refineResType r ty) = (co, ty')
79 -- Then co :: ty':=:ty
80 refineResType reft ty
81   = case refineType reft ty of
82         (ExprCoFn co, ty1) -> (ExprCoFn (mkSymCoercion co), ty1)
83         (id_co,       ty1) -> ASSERT( isIdCoercion id_co )
84                               (idCoercion, ty1)
85 \end{code}
86
87
88 %************************************************************************
89 %*                                                                      *
90                 Generating a type refinement
91 %*                                                                      *
92 %************************************************************************
93
94 \begin{code}
95 gadtRefine :: Refinement
96            -> [TyVar]   -- Bind these by preference
97            -> [CoVar]
98            -> MaybeErr Message Refinement
99 \end{code}
100
101 (gadtRefine cvs) takes a list of coercion variables, and returns a
102 list of coercions, obtained by unifying the types equated by the
103 incoming coercions.  The returned coercions all have kinds of form
104 (a:=:ty), where a is a rigid type variable.
105
106 Example:
107   gadtRefine [c :: (a,Int):=:(Bool,b)]
108   = [ right (left c) :: a:=:Bool,       
109       sym (right c)  :: b:=:Int ]
110
111 That is, given evidence 'c' that (a,Int)=(Bool,b), it returns derived
112 evidence in easy-to-use form.  In particular, given any e::ty, we know 
113 that:
114         e `cast` ty[right (left c)/a, sym (right c)/b]
115         :: ty [Bool/a, Int/b]
116       
117 Two refinements:
118
119 - It can fail, if the coercion is unsatisfiable.
120
121 - It's biased, by being given a set of type variables to bind
122   when there is a choice. Example:
123         MkT :: forall a. a -> T [a]
124         f :: forall b. T [b] -> b
125         f x = let v = case x of { MkT y -> y }
126               in ...
127   Here we want to bind [a->b], not the other way round, because
128   in this example the return type is wobbly, and we want the
129   program to typecheck
130
131
132 -- E.g. (a, Bool, right (left c))
133 -- INVARIANT: in the triple (tv, ty, co), we have (co :: tv:=:ty)
134 -- The result is idempotent: the 
135
136 \begin{code}
137 gadtRefine (Reft in_scope env1) 
138            ex_tvs co_vars
139 -- Precondition: fvs( co_vars ) # env1
140 -- That is, the kinds of the co_vars are a
141 -- fixed point of the  incoming refinement
142
143   = initUM (tryToBind tv_set) $
144     do  {       -- Run the unifier, starting with an empty env
145         ; env2 <- foldM do_one emptyInternalReft co_vars
146
147                 -- Find the fixed point of the resulting 
148                 -- non-idempotent substitution
149         ; let tmp_env = env1 `plusVarEnv` env2
150               out_env = fixTvCoEnv in_scope' tmp_env
151         ; return (Reft in_scope' out_env) }
152   where
153     tv_set = mkVarSet ex_tvs
154     in_scope' = foldr extend in_scope co_vars
155     extend co_var in_scope
156         = extendInScopeSetSet (extendInScopeSet in_scope co_var)
157                               (tyVarsOfType (tyVarKind co_var))
158         
159     do_one reft co_var = unify reft (TyVarTy co_var) ty1 ty2
160         where
161            (ty1,ty2) = splitCoercionKind (tyVarKind co_var)
162 \end{code} 
163
164 %************************************************************************
165 %*                                                                      *
166                 Unification
167 %*                                                                      *
168 %************************************************************************
169
170 \begin{code}
171 tcUnifyTys :: (TyVar -> BindFlag)
172            -> [Type] -> [Type]
173            -> Maybe TvSubst     -- A regular one-shot substitution
174 -- The two types may have common type variables, and indeed do so in the
175 -- second call to tcUnifyTys in FunDeps.checkClsFD
176 --
177 -- We implement tcUnifyTys using the evidence-generating 'unify' function
178 -- in this module, even though we don't need to generate any evidence.
179 -- This is simply to avoid replicating all all the code for unify
180 tcUnifyTys bind_fn tys1 tys2
181   = maybeErrToMaybe $ initUM bind_fn $
182     do { reft <- unifyList emptyInternalReft cos tys1 tys2
183
184         -- Find the fixed point of the resulting non-idempotent substitution
185         ; let in_scope = mkInScopeSet (tvs1 `unionVarSet` tvs2)
186               tv_env   = fixTvSubstEnv in_scope (mapVarEnv snd reft)
187
188         ; return (mkTvSubst in_scope tv_env) }
189   where
190     tvs1 = tyVarsOfTypes tys1
191     tvs2 = tyVarsOfTypes tys2
192     cos  = zipWith mkUnsafeCoercion tys1 tys2
193
194
195 ----------------------------
196 fixTvCoEnv :: InScopeSet -> InternalReft -> InternalReft
197         -- Find the fixed point of a Refinement
198         -- (assuming it has no loops!)
199 fixTvCoEnv in_scope env
200   = fixpt
201   where
202     fixpt         = mapVarEnv step env
203
204     step (co, ty) = (co1, ty')
205       -- Apply fixpt one step:
206       -- Use refineType to get a substituted type, ty', and a coercion, co_fn,
207       -- which justifies the substitution.  If the coercion is not the identity
208       -- then use transitivity with the original coercion
209       where
210         (co_fn, ty') = refineType (Reft in_scope fixpt) ty
211         co1 | ExprCoFn co'' <- co_fn = mkTransCoercion co'' co
212                                          -- This trans looks backwards, but it
213                                          -- works somehow
214             | otherwise              = ASSERT( isIdCoercion co_fn ) co 
215
216 -----------------------------
217 fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv
218 fixTvSubstEnv in_scope env
219   = fixpt 
220   where
221     fixpt = mapVarEnv (substTy (mkTvSubst in_scope fixpt)) env
222
223 ----------------------------
224 dataConCanMatch :: DataCon -> [Type] -> Bool
225 -- Returns True iff the data con can match a scrutinee of type (T tys)
226 --                  where T is the type constructor for the data con
227 --
228 -- Instantiate the equations and try to unify them
229 dataConCanMatch con tys
230   = isJust (tcUnifyTys (\tv -> BindMe) 
231                        (map (substTyVar subst . fst) eq_spec)
232                        (map snd eq_spec))
233   where
234     dc_tvs  = dataConUnivTyVars con
235     eq_spec = dataConEqSpec con
236     subst   = zipTopTvSubst dc_tvs tys
237
238 ----------------------------
239 tryToBind :: TyVarSet -> TyVar -> BindFlag
240 tryToBind tv_set tv | tv `elemVarSet` tv_set = BindMe
241                     | otherwise              = AvoidMe
242
243
244 \end{code}
245
246
247 %************************************************************************
248 %*                                                                      *
249                 The workhorse
250 %*                                                                      *
251 %************************************************************************
252
253 \begin{code}
254 type InternalReft = TyVarEnv (Coercion, Type)
255
256 -- INVARIANT:   a->(co,ty)   then   co :: (a:=:ty)
257 -- Not necessarily idemopotent
258
259 emptyInternalReft :: InternalReft
260 emptyInternalReft = emptyVarEnv
261
262 unify :: InternalReft           -- An existing substitution to extend
263       -> Coercion       -- Witness of their equality 
264       -> Type -> Type   -- Types to be unified, and witness of their equality
265       -> UM InternalReft                -- Just the extended substitution, 
266                                 -- Nothing if unification failed
267 -- We do not require the incoming substitution to be idempotent,
268 -- nor guarantee that the outgoing one is.  That's fixed up by
269 -- the wrappers.
270
271 -- PRE-CONDITION: in the call (unify r co ty1 ty2), we know that
272 --                      co :: (ty1:=:ty2)
273
274 -- Respects newtypes, PredTypes
275
276 unify subst co ty1 ty2 = -- pprTrace "unify" (ppr subst <+> pprParendType ty1 <+> pprParendType ty2) $
277                          unify_ subst co ty1 ty2
278
279 -- in unify_, any NewTcApps/Preds should be taken at face value
280 unify_ subst co (TyVarTy tv1) ty2  = uVar False subst co tv1 ty2
281 unify_ subst co ty1 (TyVarTy tv2)  = uVar True  subst co tv2 ty1
282
283 unify_ subst co ty1 ty2 | Just ty1' <- tcView ty1 = unify subst co ty1' ty2
284 unify_ subst co ty1 ty2 | Just ty2' <- tcView ty2 = unify subst co ty1 ty2'
285
286 unify_ subst co (PredTy p1) (PredTy p2) = unify_pred subst co p1 p2
287
288 unify_ subst co t1@(TyConApp tyc1 tys1) t2@(TyConApp tyc2 tys2) 
289   | tyc1 == tyc2 = unify_tys subst co tys1 tys2
290
291 unify_ subst co (FunTy ty1a ty1b) (FunTy ty2a ty2b) 
292   = do  { let [co1,co2] = decomposeCo 2 co
293         ; subst' <- unify subst co1 ty1a ty2a
294         ; unify subst' co2 ty1b ty2b }
295
296         -- Applications need a bit of care!
297         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
298         -- NB: we've already dealt with type variables and Notes,
299         -- so if one type is an App the other one jolly well better be too
300 unify_ subst co (AppTy ty1a ty1b) ty2
301   | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
302   = do  { subst' <- unify subst (mkLeftCoercion co) ty1a ty2a
303         ; unify subst' (mkRightCoercion co) ty1b ty2b }
304
305 unify_ subst co ty1 (AppTy ty2a ty2b)
306   | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
307   = do  { subst' <- unify subst (mkLeftCoercion co) ty1a ty2a
308         ; unify subst' (mkRightCoercion co) ty1b ty2b }
309
310 unify_ subst co ty1 ty2 = failWith (misMatch ty1 ty2)
311         -- ForAlls??
312
313
314 ------------------------------
315 unify_pred subst co (ClassP c1 tys1) (ClassP c2 tys2)
316   | c1 == c2 = unify_tys subst co tys1 tys2
317 unify_pred subst co (IParam n1 t1) (IParam n2 t2)
318   | n1 == n2 = unify subst co t1 t2
319 unify_pred subst co p1 p2 = failWith (misMatch (PredTy p1) (PredTy p2))
320  
321 ------------------------------
322 unify_tys :: InternalReft -> Coercion -> [Type] -> [Type] -> UM InternalReft
323 unify_tys subst co xs ys
324   = unifyList subst (decomposeCo (length xs) co) xs ys
325
326 unifyList :: InternalReft -> [Coercion] -> [Type] -> [Type] -> UM InternalReft
327 unifyList subst orig_cos orig_xs orig_ys
328   = go subst orig_cos orig_xs orig_ys
329   where
330     go subst _        []     []     = return subst
331     go subst (co:cos) (x:xs) (y:ys) = do { subst' <- unify subst co x y
332                                          ; go subst' cos xs ys }
333     go subst _ _ _ = failWith (lengthMisMatch orig_xs orig_ys)
334
335 ---------------------------------
336 uVar :: Bool            -- Swapped
337      -> InternalReft    -- An existing substitution to extend
338      -> Coercion
339      -> TyVar           -- Type variable to be unified
340      -> Type            -- with this type
341      -> UM InternalReft
342
343 -- PRE-CONDITION: in the call (uVar swap r co tv1 ty), we know that
344 --      if swap=False   co :: (tv1:=:ty)
345 --      if swap=True    co :: (ty:=:tv1)
346
347 uVar swap subst co tv1 ty
348  = -- Check to see whether tv1 is refined by the substitution
349    case (lookupVarEnv subst tv1) of
350
351      -- Yes, call back into unify'
352      Just (co',ty')     -- co' :: (tv1:=:ty')
353         | swap          -- co :: (ty:=:tv1)
354         -> unify subst (mkTransCoercion co co') ty ty' 
355         | otherwise     -- co :: (tv1:=:ty)
356         -> unify subst (mkTransCoercion (mkSymCoercion co') co) ty' ty
357
358      -- No, continue
359      Nothing -> uUnrefined subst (if swap then mkSymCoercion co else co)
360                            tv1 ty ty
361
362
363 uUnrefined :: InternalReft        -- An existing substitution to extend
364            -> Coercion
365            -> TyVar               -- Type variable to be unified
366            -> Type                -- with this type
367            -> Type                -- (de-noted version)
368            -> UM InternalReft
369
370 -- We know that tv1 isn't refined
371 -- PRE-CONDITION: in the call (uUnrefined r co tv ty ty'), we know that
372 --      co :: tv:=:ty
373
374 uUnrefined subst co tv1 ty2 ty2'
375   | Just ty2'' <- tcView ty2'
376   = uUnrefined subst co tv1 ty2 ty2''   -- Unwrap synonyms
377                 -- This is essential, in case we have
378                 --      type Foo a = a
379                 -- and then unify a :=: Foo a
380
381 uUnrefined subst co tv1 ty2 (TyVarTy tv2)
382   | tv1 == tv2          -- Same type variable
383   = return subst
384
385     -- Check to see whether tv2 is refined
386   | Just (co',ty') <- lookupVarEnv subst tv2
387   = uUnrefined subst (mkTransCoercion co co') tv1 ty' ty'
388
389   -- So both are unrefined; next, see if the kinds force the direction
390   | eqKind k1 k2        -- Can update either; so check the bind-flags
391   = do  { b1 <- tvBindFlag tv1
392         ; b2 <- tvBindFlag tv2
393         ; case (b1,b2) of
394             (BindMe, _)          -> bind False tv1 ty2
395
396             (AvoidMe, BindMe)    -> bind True tv2 ty1
397             (AvoidMe, _)         -> bind False tv1 ty2
398
399             (WildCard, WildCard) -> return subst
400             (WildCard, Skolem)   -> return subst
401             (WildCard, _)        -> bind True tv2 ty1
402
403             (Skolem, WildCard)   -> return subst
404             (Skolem, Skolem)     -> failWith (misMatch ty1 ty2)
405             (Skolem, _)          -> bind True tv2 ty1
406         }
407
408   | k1 `isSubKind` k2 = bindTv subst (mkSymCoercion co) tv2 ty1 -- Must update tv2
409   | k2 `isSubKind` k1 = bindTv subst co tv1 ty2 -- Must update tv1
410
411   | otherwise = failWith (kindMisMatch tv1 ty2)
412   where
413     ty1 = TyVarTy tv1
414     k1 = tyVarKind tv1
415     k2 = tyVarKind tv2
416     bind swap tv ty = 
417         ASSERT2( (coercionKindPredTy co1 `tcEqType` mkCoKind (mkTyVarTy tv) ty)
418                , (text "Refinement invariant failure: co = " <+> ppr co  <+> ppr (coercionKindPredTy co) $$ text "subst = " <+> ppr tv <+> ppr (mkCoKind (mkTyVarTy tv) ty)))
419         return (extendVarEnv subst tv (co1,ty))
420       where
421         co1 = if swap then mkSymCoercion co else co
422
423 uUnrefined subst co tv1 ty2 ty2'        -- ty2 is not a type variable
424   | tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2')
425   = failWith (occursCheck tv1 ty2)      -- Occurs check
426   | not (k2 `isSubKind` k1)
427   = failWith (kindMisMatch tv1 ty2)     -- Kind check
428   | otherwise
429   = bindTv subst co tv1 ty2             -- Bind tyvar to the synonym if poss
430   where
431     k1 = tyVarKind tv1
432     k2 = typeKind ty2'
433
434 substTvSet :: InternalReft -> TyVarSet -> TyVarSet
435 -- Apply the non-idempotent substitution to a set of type variables,
436 -- remembering that the substitution isn't necessarily idempotent
437 substTvSet subst tvs
438   = foldVarSet (unionVarSet . get) emptyVarSet tvs
439   where
440     get tv = case lookupVarEnv subst tv of
441                 Nothing     -> unitVarSet tv
442                 Just (_,ty) -> substTvSet subst (tyVarsOfType ty)
443
444 bindTv subst co tv ty   -- ty is not a type variable
445   = ASSERT2( (coercionKindPredTy co `tcEqType` mkCoKind (mkTyVarTy tv) ty), 
446           (text "Refinement invariant failure: co = " <+> ppr co  <+> ppr (coercionKindPredTy co) $$ text "subst = " <+> ppr tv <+> ppr (mkCoKind (mkTyVarTy tv) ty))  )
447     do  { b <- tvBindFlag tv
448         ; case b of
449             Skolem   -> failWith (misMatch (TyVarTy tv) ty)
450             WildCard -> return subst
451             other    -> return (extendVarEnv subst tv (co,ty))
452         }
453 \end{code}
454
455 %************************************************************************
456 %*                                                                      *
457                 Unification monad
458 %*                                                                      *
459 %************************************************************************
460
461 \begin{code}
462 data BindFlag 
463   = BindMe      -- A regular type variable
464   | AvoidMe     -- Like BindMe but, given the choice, avoid binding it
465
466   | Skolem      -- This type variable is a skolem constant
467                 -- Don't bind it; it only matches itself
468
469   | WildCard    -- This type variable matches anything,
470                 -- and does not affect the substitution
471
472 newtype UM a = UM { unUM :: (TyVar -> BindFlag)
473                          -> MaybeErr Message a }
474
475 instance Monad UM where
476   return a = UM (\tvs -> Succeeded a)
477   fail s   = UM (\tvs -> Failed (text s))
478   m >>= k  = UM (\tvs -> case unUM m tvs of
479                            Failed err -> Failed err
480                            Succeeded v  -> unUM (k v) tvs)
481
482 initUM :: (TyVar -> BindFlag) -> UM a -> MaybeErr Message a
483 initUM badtvs um = unUM um badtvs
484
485 tvBindFlag :: TyVar -> UM BindFlag
486 tvBindFlag tv = UM (\tv_fn -> Succeeded (tv_fn tv))
487
488 failWith :: Message -> UM a
489 failWith msg = UM (\tv_fn -> Failed msg)
490
491 maybeErrToMaybe :: MaybeErr fail succ -> Maybe succ
492 maybeErrToMaybe (Succeeded a) = Just a
493 maybeErrToMaybe (Failed m)    = Nothing
494 \end{code}
495
496
497 %************************************************************************
498 %*                                                                      *
499                 Error reporting
500         We go to a lot more trouble to tidy the types
501         in TcUnify.  Maybe we'll end up having to do that
502         here too, but I'll leave it for now.
503 %*                                                                      *
504 %************************************************************************
505
506 \begin{code}
507 misMatch t1 t2
508   = ptext SLIT("Can't match types") <+> quotes (ppr t1) <+> 
509     ptext SLIT("and") <+> quotes (ppr t2)
510
511 lengthMisMatch tys1 tys2
512   = sep [ptext SLIT("Can't match unequal length lists"), 
513          nest 2 (ppr tys1), nest 2 (ppr tys2) ]
514
515 kindMisMatch tv1 t2
516   = vcat [ptext SLIT("Can't match kinds") <+> quotes (ppr (tyVarKind tv1)) <+> 
517             ptext SLIT("and") <+> quotes (ppr (typeKind t2)),
518           ptext SLIT("when matching") <+> quotes (ppr tv1) <+> 
519                 ptext SLIT("with") <+> quotes (ppr t2)]
520
521 occursCheck tv ty
522   = hang (ptext SLIT("Can't construct the infinite type"))
523        2 (ppr tv <+> equals <+> ppr ty)
524 \end{code}