compiler/typecheck/TcTyFuns.lhs

   1
   2 \begin{code}
   3 module TcTyFuns (
   4         tcNormalizeFamInst,
   5
   6         normaliseGivens, normaliseGivenDicts,
   7         normaliseWanteds, normaliseWantedDicts,
   8         solveWanteds,
   9         substEqInDictInsts,
  10
  11         addBind                 -- should not be here
  12   ) where
  13
  14
  15 #include "HsVersions.h"
  16
  17 import HsSyn
  18
  19 import TcRnMonad
  20 import TcEnv
  21 import Inst
  22 import TcType
  23 import TcMType
  24 import Coercion
  25 import TypeRep  ( Type(..) )
  26 import TyCon
  27 import Var      ( isTcTyVar )
  28 import Type
  29 import Bag
  30 import Outputable
  31 import SrcLoc   ( Located(..) )
  32 import Maybes
  33
  34 import Data.List
  35 import Control.Monad (liftM)
  36 \end{code}
  37
  38
  39 %************************************************************************
  40 %*                                                                      *
  41                 Normalisation of types
  42 %*                                                                      *
  43 %************************************************************************
  44
  45 Unfold a single synonym family instance and yield the witnessing coercion.
  46 Return 'Nothing' if the given type is either not synonym family instance
  47 or is a synonym family instance that has no matching instance declaration.
  48 (Applies only if the type family application is outermost.)
  49
  50 For example, if we have
  51
  52   :Co:R42T a :: T [a] ~ :R42T a
  53
  54 then 'T [Int]' unfolds to (:R42T Int, :Co:R42T Int).
  55
  56 \begin{code}
  57 tcUnfoldSynFamInst :: Type -> TcM (Maybe (Type, Coercion))
  58 tcUnfoldSynFamInst (TyConApp tycon tys)
  59   | not (isOpenSynTyCon tycon)     -- unfold *only* _synonym_ family instances
  60   = return Nothing
  61   | otherwise
  62   = do { -- we only use the indexing arguments for matching,
  63          -- not the additional ones
  64        ; maybeFamInst <- tcLookupFamInst tycon idxTys
  65        ; case maybeFamInst of
  66            Nothing                -> return Nothing
  67            Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc tys',
  68                                                     mkTyConApp coe_tc tys')
  69              where
  70                tys'   = rep_tys ++ restTys
  71                coe_tc = expectJust "TcTyFun.tcUnfoldSynFamInst"
  72                                    (tyConFamilyCoercion_maybe rep_tc)
  73        }
  74     where
  75         n                = tyConArity tycon
  76         (idxTys, restTys) = splitAt n tys
  77 tcUnfoldSynFamInst _other = return Nothing
  78 \end{code}
  79
  80 Normalise 'Type's and 'PredType's by unfolding type family applications where
  81 possible (ie, we treat family instances as a TRS).  Also zonk meta variables.
  82
  83         tcNormalizeFamInst ty = (co, ty')
  84         then   co : ty ~ ty'
  85
  86 \begin{code}
  87 tcNormalizeFamInst :: Type -> TcM (CoercionI, Type)
  88 tcNormalizeFamInst = tcGenericNormalizeFamInst tcUnfoldSynFamInst
  89
  90 tcNormalizeFamInstPred :: TcPredType -> TcM (CoercionI, TcPredType)
  91 tcNormalizeFamInstPred = tcGenericNormalizeFamInstPred tcUnfoldSynFamInst
  92 \end{code}
  93
  94 Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
  95 apply the normalisation function gives as the first argument to every TyConApp
  96 and every TyVarTy subterm.
  97
  98         tcGenericNormalizeFamInst fun ty = (co, ty')
  99         then   co : ty ~ ty'
 100
 101 This function is (by way of using smart constructors) careful to ensure that
 102 the returned coercion is exactly IdCo (and not some semantically equivalent,
 103 but syntactically different coercion) whenever (ty' `tcEqType` ty).  This
 104 makes it easy for the caller to determine whether the type changed.  BUT
 105 even if we return IdCo, ty' may be *syntactically* different from ty due to
 106 unfolded closed type synonyms (by way of tcCoreView).  In the interest of
 107 good error messages, callers should discard ty' in favour of ty in this case.
 108
 109 \begin{code}
 110 tcGenericNormalizeFamInst :: (TcType -> TcM (Maybe (TcType,Coercion)))
 111                              -- what to do with type functions and tyvars
 112                            -> TcType                    -- old type
 113                            -> TcM (CoercionI, Type)     -- (coercion, new type)
 114 tcGenericNormalizeFamInst fun ty
 115   | Just ty' <- tcView ty = tcGenericNormalizeFamInst fun ty'
 116 tcGenericNormalizeFamInst fun (TyConApp tyCon tys)
 117   = do  { (cois, ntys) <- mapAndUnzipM (tcGenericNormalizeFamInst fun) tys
 118         ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
 119         ; maybe_ty_co <- fun (TyConApp tyCon ntys)      -- use normalised args!
 120         ; case maybe_ty_co of
 121             -- a matching family instance exists
 122             Just (ty', co) ->
 123               do { let first_coi = mkTransCoI tycon_coi (ACo co)
 124                  ; (rest_coi, nty) <- tcGenericNormalizeFamInst fun ty'
 125                  ; let fix_coi = mkTransCoI first_coi rest_coi
 126                  ; return (fix_coi, nty)
 127                  }
 128             -- no matching family instance exists
 129             -- we do not do anything
 130             Nothing -> return (tycon_coi, TyConApp tyCon ntys)
 131         }
 132 tcGenericNormalizeFamInst fun (AppTy ty1 ty2)
 133   = do  { (coi1,nty1) <- tcGenericNormalizeFamInst fun ty1
 134         ; (coi2,nty2) <- tcGenericNormalizeFamInst fun ty2
 135         ; return (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2)
 136         }
 137 tcGenericNormalizeFamInst fun (FunTy ty1 ty2)
 138   = do  { (coi1,nty1) <- tcGenericNormalizeFamInst fun ty1
 139         ; (coi2,nty2) <- tcGenericNormalizeFamInst fun ty2
 140         ; return (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2)
 141         }
 142 tcGenericNormalizeFamInst fun (ForAllTy tyvar ty1)
 143   = do  { (coi,nty1) <- tcGenericNormalizeFamInst fun ty1
 144         ; return (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
 145         }
 146 tcGenericNormalizeFamInst fun (NoteTy note ty1)
 147   = do  { (coi,nty1) <- tcGenericNormalizeFamInst fun ty1
 148         ; return (mkNoteTyCoI note coi,NoteTy note nty1)
 149         }
 150 tcGenericNormalizeFamInst fun ty@(TyVarTy tv)
 151   | isTcTyVar tv
 152   = do  { traceTc (text "tcGenericNormalizeFamInst" <+> ppr ty)
 153         ; res <- lookupTcTyVar tv
 154         ; case res of
 155             DoneTv _ ->
 156               do { maybe_ty' <- fun ty
 157                  ; case maybe_ty' of
 158                      Nothing         -> return (IdCo, ty)
 159                      Just (ty', co1) ->
 160                        do { (coi2, ty'') <- tcGenericNormalizeFamInst fun ty'
 161                           ; return (ACo co1 `mkTransCoI` coi2, ty'')
 162                           }
 163                  }
 164             IndirectTv ty' -> tcGenericNormalizeFamInst fun ty'
 165         }
 166   | otherwise
 167   = return (IdCo, ty)
 168 tcGenericNormalizeFamInst fun (PredTy predty)
 169   = do  { (coi, pred') <- tcGenericNormalizeFamInstPred fun predty
 170         ; return (coi, PredTy pred') }
 171
 172 ---------------------------------
 173 tcGenericNormalizeFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
 174                               -> TcPredType
 175                               -> TcM (CoercionI, TcPredType)
 176
 177 tcGenericNormalizeFamInstPred fun (ClassP cls tys)
 178   = do { (cois, tys')<- mapAndUnzipM (tcGenericNormalizeFamInst fun) tys
 179        ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
 180        }
 181 tcGenericNormalizeFamInstPred fun (IParam ipn ty)
 182   = do { (coi, ty') <- tcGenericNormalizeFamInst fun ty
 183        ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
 184        }
 185 tcGenericNormalizeFamInstPred fun (EqPred ty1 ty2)
 186   = do { (coi1, ty1') <- tcGenericNormalizeFamInst fun ty1
 187        ; (coi2, ty2') <- tcGenericNormalizeFamInst fun ty2
 188        ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
 189 \end{code}
 190
 191
 192 %************************************************************************
 193 %*                                                                      *
 194 \section{Normalisation of Given Dictionaries}
 195 %*                                                                      *
 196 %************************************************************************
 197
 198 \begin{code}
 199 normaliseGivenDicts, normaliseWantedDicts
 200         :: [Inst]               -- given equations
 201         -> [Inst]               -- dictionaries
 202         -> TcM ([Inst],TcDictBinds)
 203
 204 normaliseGivenDicts  eqs dicts = normalise_dicts eqs dicts False
 205 normaliseWantedDicts eqs dicts = normalise_dicts eqs dicts True
 206
 207 normalise_dicts
 208         :: [Inst]       -- given equations
 209         -> [Inst]       -- dictionaries
 210         -> Bool         -- True <=> the dicts are wanted
 211                         -- Fals <=> they are given
 212         -> TcM ([Inst],TcDictBinds)
 213 normalise_dicts given_eqs dicts is_wanted
 214   = do  { traceTc $ text "normaliseGivenDicts <-" <+> ppr dicts <+>
 215                     text "with" <+> ppr given_eqs
 216         ; (dicts0, binds0)  <- normaliseInsts is_wanted dicts
 217         ; (dicts1, binds1)  <- substEqInDictInsts given_eqs dicts0
 218         ; let binds01 = binds0 `unionBags` binds1
 219         ; if isEmptyBag binds1
 220           then return (dicts1, binds01)
 221           else do { (dicts2, binds2) <- normaliseGivenDicts given_eqs dicts1
 222                   ; return (dicts2, binds01 `unionBags` binds2) } }
 223 \end{code}
 224
 225
 226 %************************************************************************
 227 %*                                                                      *
 228 \section{Normalisation of wanteds constraints}
 229 %*                                                                      *
 230 %************************************************************************
 231
 232 \begin{code}
 233 normaliseWanteds :: [Inst] -> TcM [Inst]
 234 normaliseWanteds insts
 235   = do { traceTc (text "normaliseWanteds <-" <+> ppr insts)
 236        ; result <- liftM fst $ rewriteToFixedPoint Nothing
 237                      [ ("(Occurs)",  noChange  $ occursCheckInsts)
 238                      , ("(ZONK)",    dontRerun $ zonkInsts)
 239                      , ("(TRIVIAL)", trivialInsts)
 240                      -- no `swapInsts'; it messes up error messages and should
 241                      -- not be necessary -=chak
 242                      , ("(DECOMP)",  decompInsts)
 243                      , ("(TOP)",     topInsts)
 244                      , ("(SUBST)",   substInsts)
 245                      , ("(UNIFY)",   unifyInsts)
 246                      ] insts
 247        ; traceTc (text "normaliseWanteds ->" <+> ppr result)
 248        ; return result
 249        }
 250 \end{code}
 251
 252
 253 %************************************************************************
 254 %*                                                                      *
 255 \section{Normalisation of givens constraints}
 256 %*                                                                      *
 257 %************************************************************************
 258
 259 \begin{code}
 260 normaliseGivens :: [Inst] -> TcM ([Inst], TcM ())
 261 normaliseGivens givens
 262  = do { traceTc (text "normaliseGivens <-" <+> ppr givens)
 263       ; (result, deSkolem) <-
 264           rewriteToFixedPoint (Just ("(SkolemOccurs)", skolemOccurs))
 265             [ ("(Occurs)",  noChange  $ occursCheckInsts)
 266             , ("(ZONK)",    dontRerun $ zonkInsts)
 267             , ("(TRIVIAL)", trivialInsts)
 268             , ("(SWAP)",    swapInsts)
 269             , ("(DECOMP)",  decompInsts)
 270             , ("(TOP)",     topInsts)
 271             , ("(SUBST)",   substInsts)
 272             ] givens
 273       ; traceTc (text "normaliseGivens ->" <+> ppr result)
 274       ; return (result, deSkolem)
 275       }
 276
 277 -- An explanation of what this does would be helpful! -=chak
 278 skolemOccurs :: PrecondRule
 279 skolemOccurs [] = return ([], return ())
 280 skolemOccurs (inst@(EqInst {}):insts)
 281         = do { (insts',actions) <- skolemOccurs insts
 282                -- check whether the current inst  co :: ty1 ~ ty2  suffers
 283                -- from the occurs check issue: F ty1 \in ty2
 284               ; let occurs = go False ty2
 285               ; if occurs
 286                   then
 287                       -- if it does generate two new coercions:
 288                       do { skolem_var <- newMetaTyVar TauTv (typeKind ty1)
 289                          ; let skolem_ty = TyVarTy skolem_var
 290                       --    ty1    :: ty1 ~ b
 291                          ; inst1 <- mkEqInst (EqPred ty1 skolem_ty) (mkGivenCo ty1)
 292                       --    sym co :: ty2 ~ b
 293                          ; inst2 <- mkEqInst (EqPred ty2 skolem_ty) (mkGivenCo $ fromACo $ mkSymCoI $ ACo $ fromGivenCo co)
 294                       -- to replace the old one
 295                       -- the corresponding action is
 296                       --    b := ty1
 297                          ; let action = writeMetaTyVar skolem_var ty1
 298                          ; return (inst1:inst2:insts', action >> actions)
 299                          }
 300                   else
 301                       return (inst:insts', actions)
 302              }
 303         where
 304                 ty1 = eqInstLeftTy inst
 305                 ty2 = eqInstRightTy inst
 306                 co  = eqInstCoercion inst
 307                 check :: Bool -> TcType -> Bool
 308                 check flag ty
 309                         = if flag && ty1 `tcEqType` ty
 310                                 then True
 311                                 else go flag ty
 312
 313                 go flag (TyConApp con tys)      = or $ map (check (isOpenSynTyCon con || flag)) tys
 314                 go flag (FunTy arg res) = or $ map (check flag) [arg,res]
 315                 go flag (AppTy fun arg)         = or $ map (check flag) [fun,arg]
 316                 go _    _                       = False
 317 skolemOccurs _ = panic "TcTyFuns.skolemOccurs: not EqInst"
 318 \end{code}
 319
 320
 321 %************************************************************************
 322 %*                                                                      *
 323 \section{Solving of wanted constraints with respect to a given set}
 324 %*                                                                      *
 325 %************************************************************************
 326
 327 \begin{code}
 328 solveWanteds :: [Inst]          -- givens
 329              -> [Inst]          -- wanteds
 330              -> TcM [Inst]      -- irreducible wanteds
 331 solveWanteds givens wanteds
 332   = do { traceTc $ text "solveWanteds <-" <+> ppr wanteds <+> text "with" <+>
 333                    ppr givens
 334        ; result <- liftM fst $ rewriteToFixedPoint Nothing
 335                      [ ("(Occurs)",  noChange $ occursCheckInsts)
 336                      , ("(TRIVIAL)", trivialInsts)
 337                      , ("(DECOMP)",  decompInsts)
 338                      , ("(TOP)",     topInsts)
 339                      , ("(GIVEN)",   givenInsts givens)
 340                      , ("(UNIFY)",   unifyInsts)
 341                      ] wanteds
 342        ; traceTc (text "solveWanteds ->" <+> ppr result)
 343        ; return result
 344        }
 345   where
 346     -- Use `substInst' with every given on all the wanteds.
 347     givenInsts :: [Inst] -> [Inst] -> TcM ([Inst],Bool)
 348     givenInsts []     wanteds = return (wanteds,False)
 349     givenInsts (g:gs) wanteds
 350       = do { (wanteds1, changed1) <- givenInsts gs wanteds
 351            ; (wanteds2, changed2) <- substInst g wanteds1
 352            ; return (wanteds2, changed1 || changed2)
 353            }
 354 \end{code}
 355
 356
 357 %************************************************************************
 358 %*                                                                      *
 359 \section{Normalisation rules and iterative rule application}
 360 %*                                                                      *
 361 %************************************************************************
 362
 363 We have four kinds of normalising rewrite rules:
 364
 365 (1) Normalisation rules that rewrite a set of insts and return a flag indicating
 366     whether any changes occurred during rewriting that necessitate re-running
 367     the current rule set.
 368
 369 (2) Precondition rules that rewrite a set of insts and return a monadic action
 370     that reverts the effect of preconditioning.
 371
 372 (3) Idempotent normalisation rules that never require re-running the rule set.
 373
 374 (4) Checking rule that does not alter the set of insts.
 375
 376 \begin{code}
 377 type RewriteRule     = [Inst] -> TcM ([Inst], Bool)   -- rewrite, maybe re-run
 378 type PrecondRule     = [Inst] -> TcM ([Inst], TcM ()) -- rewrite, revertable
 379 type IdemRewriteRule = [Inst] -> TcM [Inst]           -- rewrite, don't re-run
 380 type CheckRule       = [Inst] -> TcM ()               -- check
 381
 382 type NamedRule       = (String, RewriteRule)          -- rule with description
 383 type NamedPreRule    = (String, PrecondRule)          -- precond with desc
 384 \end{code}
 385
 386 Templates lifting idempotent and checking rules to full rules (which can be put
 387 into a rule set).
 388
 389 \begin{code}
 390 dontRerun :: IdemRewriteRule -> RewriteRule
 391 dontRerun rule insts = liftM addFalse $ rule insts
 392   where
 393     addFalse x = (x, False)
 394
 395 noChange :: CheckRule -> RewriteRule
 396 noChange rule insts = rule insts >> return (insts, False)
 397 \end{code}
 398
 399 The following function applies a set of rewrite rules until a fixed point is
 400 reached; i.e., none of the `RewriteRule's require re-running the rule set.
 401 Optionally, there may be a pre-conditing rule that is applied before any other
 402 rules are applied and before the rule set is re-run.
 403
 404 The result is the set of rewritten (i.e., normalised) insts and, in case of a
 405 pre-conditing rule, a monadic action that reverts the effects of
 406 pre-conditioning - specifically, this is removing introduced skolems.
 407
 408 \begin{code}
 409 rewriteToFixedPoint :: Maybe NamedPreRule   -- optional preconditioning rule
 410                     -> [NamedRule]          -- rule set
 411                     -> [Inst]               -- insts to rewrite
 412                     -> TcM ([Inst], TcM ())
 413 rewriteToFixedPoint precondRule rules insts
 414   = completeRewrite (return ()) precondRule insts
 415   where
 416     completeRewrite :: TcM () -> Maybe NamedPreRule -> [Inst]
 417                     -> TcM ([Inst], TcM ())
 418     completeRewrite dePrecond (Just (precondName, precond)) insts
 419       = do { (insts', dePrecond') <- precond insts
 420            ; traceTc $ text precondName <+> ppr insts'
 421            ; tryRules (dePrecond >> dePrecond') rules insts'
 422            }
 423     completeRewrite dePrecond Nothing insts
 424       = tryRules dePrecond rules insts
 425
 426     tryRules dePrecond _                    []    = return ([]   , dePrecond)
 427     tryRules dePrecond []                   insts = return (insts, dePrecond)
 428     tryRules dePrecond ((name, rule):rules) insts
 429       = do { (insts', rerun) <- rule insts
 430            ; traceTc $ text name <+> ppr insts'
 431            ; if rerun then completeRewrite dePrecond precondRule insts'
 432                       else tryRules dePrecond rules insts'
 433            }
 434 \end{code}
 435
 436
 437 %************************************************************************
 438 %*                                                                      *
 439 \section{Different forms of Inst rewritings}
 440 %*                                                                      *
 441 %************************************************************************
 442
 443 Rewrite schemata applied by way of eq_rewrite and friends.
 444
 445 \begin{code}
 446
 447         -- (Trivial)
 448         --      g1 : t ~ t
 449         --              >-->
 450         --      g1 := t
 451         --
 452 trivialInsts :: RewriteRule
 453 trivialInsts []
 454         = return ([],False)
 455 trivialInsts (i@(EqInst {}):is)
 456         = do { (is',changed)<- trivialInsts is
 457              ; if tcEqType ty1 ty2
 458                   then do { eitherEqInst i
 459                                 (\covar -> writeMetaTyVar covar ty1)
 460                                 (\_     -> return ())
 461                           ; return (is',True)
 462                           }
 463                   else return (i:is',changed)
 464              }
 465         where
 466            ty1 = eqInstLeftTy i
 467            ty2 = eqInstRightTy i
 468 trivialInsts _ = panic "TcTyFuns.trivialInsts: not EqInst"
 469
 470 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 471 swapInsts :: RewriteRule
 472 -- All the inputs and outputs are equalities
 473 swapInsts insts
 474   = do { (insts', changeds) <- mapAndUnzipM swapInst insts
 475        ; return (insts', or changeds)
 476        }
 477
 478         -- (Swap)
 479         --      g1 : c ~ Fd
 480         --              >-->
 481         --      g2 : Fd ~ c
 482         --      g1 := sym g2
 483         --
 484         -- This is not all, is it?  Td ~ c is also rewritten to c ~ Td!
 485 swapInst :: Inst -> TcM (Inst, Bool)
 486 swapInst i@(EqInst {})
 487         = go ty1 ty2
 488         where
 489               ty1 = eqInstLeftTy i
 490               ty2 = eqInstRightTy i
 491               go ty1 ty2                | Just ty1' <- tcView ty1
 492                                         = go ty1' ty2
 493               go ty1 ty2                | Just ty2' <- tcView ty2
 494                                         = go ty1 ty2'
 495               go (TyConApp tyCon _) _   | isOpenSynTyCon tyCon
 496                                         = return (i,False)
 497                 -- we should swap!
 498               go ty1 ty2@(TyConApp tyCon _)
 499                                         | isOpenSynTyCon tyCon
 500                                         = actual_swap ty1 ty2
 501               go ty1@(TyConApp _ _) ty2@(TyVarTy _)
 502                                         = actual_swap ty1 ty2
 503               go _ _                    = return (i,False)
 504
 505               actual_swap ty1 ty2 = do { wg_co <- eitherEqInst i
 506                                                           -- old_co := sym new_co
 507                                                           (\old_covar ->
 508                                                            do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty2 ty1)
 509                                                               ; let new_co = TyVarTy new_cotv
 510                                                               ; writeMetaTyVar old_covar (mkCoercion symCoercionTyCon [new_co])
 511                                                               ; return $ mkWantedCo new_cotv
 512                                                               })
 513                                                           -- new_co := sym old_co
 514                                                           (\old_co -> return $ mkGivenCo $ mkCoercion symCoercionTyCon [old_co])
 515                                              ; new_inst <- mkEqInst (EqPred ty2 ty1) wg_co
 516                                              ; return (new_inst,True)
 517                                              }
 518 swapInst _ = panic "TcTyFuns.swapInst: not EqInst"
 519
 520 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 521 decompInsts :: RewriteRule
 522 decompInsts insts = do { (insts,bs) <- mapAndUnzipM decompInst insts
 523                        ; return (concat insts,or bs)
 524                        }
 525
 526         -- (Decomp)
 527         --      g1 : T cs ~ T ds
 528         --              >-->
 529         --      g21 : c1 ~ d1, ..., g2n : cn ~ dn
 530         --      g1 := T g2s
 531         --
 532         --  Works also for the case where T is actually an application of a
 533         --  type family constructor to a set of types, provided the
 534         --  applications on both sides of the ~ are identical;
 535         --  see also Note [OpenSynTyCon app] in TcUnify
 536         --
 537 decompInst :: Inst -> TcM ([Inst],Bool)
 538 decompInst i@(EqInst {})
 539   = go ty1 ty2
 540   where
 541     ty1 = eqInstLeftTy i
 542     ty2 = eqInstRightTy i
 543     go ty1 ty2
 544       | Just ty1' <- tcView ty1 = go ty1' ty2
 545       | Just ty2' <- tcView ty2 = go ty1 ty2'
 546
 547     go ty1@(TyConApp con1 tys1) ty2@(TyConApp con2 tys2)
 548       | con1 == con2 && identicalHead
 549       = do { cos <- eitherEqInst i
 550                       -- old_co := Con1 cos
 551                       (\old_covar ->
 552                         do { cotvs <- zipWithM (\t1 t2 ->
 553                                                 newMetaTyVar TauTv
 554                                                              (mkCoKind t1 t2))
 555                                                tys1 tys2
 556                            ; let cos = map TyVarTy cotvs
 557                            ; writeMetaTyVar old_covar (TyConApp con1 cos)
 558                            ; return $ map mkWantedCo cotvs
 559                            })
 560                       -- co_i := Con_i old_co
 561                       (\old_co -> return $
 562                                     map mkGivenCo $
 563                                         mkRightCoercions (length tys1) old_co)
 564            ; insts <- zipWithM mkEqInst (zipWith EqPred tys1 tys2) cos
 565            ; traceTc (text "decomp identicalHead" <+> ppr insts)
 566            ; return (insts, not $ null insts)
 567            }
 568       | con1 /= con2 && not (isOpenSynTyCon con1 || isOpenSynTyCon con2)
 569         -- not matching data constructors (of any flavour) are bad news
 570       = do { env0 <- tcInitTidyEnv
 571            ; let (env1, tidy_ty1) = tidyOpenType env0 ty1
 572                  (env2, tidy_ty2) = tidyOpenType env1 ty2
 573                  extra            = sep [ppr tidy_ty1, char '~', ppr tidy_ty2]
 574                  msg              =
 575                    ptext SLIT("Unsolvable equality constraint:")
 576            ; failWithTcM (env2, hang msg 2 extra)
 577            }
 578       where
 579         n             = tyConArity con1
 580         (idxTys1, _)  = splitAt n tys1
 581         (idxTys2, _)  = splitAt n tys2
 582         identicalHead = not (isOpenSynTyCon con1) ||
 583                         idxTys1 `tcEqTypes` idxTys2
 584
 585     go _ _ = return ([i], False)
 586 decompInst _ = panic "TcTyFuns.decompInst: not EqInst"
 587
 588 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 589 topInsts :: RewriteRule
 590 topInsts insts
 591         =  do { (insts,bs) <- mapAndUnzipM topInst insts
 592               ; return (insts,or bs)
 593               }
 594
 595         -- (Top)
 596         --      g1 : t ~ s
 597         --              >--> co1 :: t ~ t' / co2 :: s ~ s'
 598         --      g2 : t' ~ s'
 599         --      g1 := co1 * g2 * sym co2
 600 topInst :: Inst -> TcM (Inst,Bool)
 601 topInst i@(EqInst {})
 602         = do { (coi1,ty1') <- tcNormalizeFamInst ty1
 603              ; (coi2,ty2') <- tcNormalizeFamInst ty2
 604              ; case (coi1,coi2) of
 605                 (IdCo,IdCo) ->
 606                   return (i,False)
 607                 _           ->
 608                  do { wg_co <- eitherEqInst i
 609                                  -- old_co = co1 * new_co * sym co2
 610                                  (\old_covar ->
 611                                   do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty1 ty2)
 612                                      ; let new_co = TyVarTy new_cotv
 613                                      ; let old_coi = coi1 `mkTransCoI` ACo new_co `mkTransCoI` (mkSymCoI coi2)
 614                                      ; writeMetaTyVar old_covar (fromACo old_coi)
 615                                      ; return $ mkWantedCo new_cotv
 616                                      })
 617                                  -- new_co = sym co1 * old_co * co2
 618                                  (\old_co -> return $ mkGivenCo $ fromACo $ mkSymCoI coi1 `mkTransCoI` ACo old_co `mkTransCoI` coi2)
 619                     ; new_inst <- mkEqInst (EqPred ty1' ty2') wg_co
 620                     ; return (new_inst,True)
 621                     }
 622              }
 623         where
 624               ty1 = eqInstLeftTy i
 625               ty2 = eqInstRightTy i
 626 topInst _ = panic "TcTyFuns.topInsts: not EqInst"
 627
 628 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 629 substInsts :: RewriteRule
 630 substInsts insts = substInstsWorker insts []
 631
 632 substInstsWorker :: [Inst] -> [Inst] -> TcM ([Inst],Bool)
 633 substInstsWorker [] acc
 634         = return (acc,False)
 635 substInstsWorker (i:is) acc
 636         | (TyConApp con _) <- tci_left i, isOpenSynTyCon con
 637         = do { (is',change) <- substInst i (acc ++ is)
 638              ; if change
 639                   then return ((i:is'),True)
 640                   else substInstsWorker is (i:acc)
 641              }
 642         | otherwise
 643         = substInstsWorker is (i:acc)
 644
 645         -- (Subst)
 646         --      g : F c ~ t,
 647         --      forall g1 : s1{F c} ~ s2{F c}
 648         --              >-->
 649         --      g2 : s1{t} ~ s2{t}
 650         --      g1 := s1{g} * g2  * sym s2{g}           <=>     g2 := sym s1{g} * g1 * s2{g}
 651 substInst :: Inst -> [Inst] -> TcM ([Inst], Bool)
 652 substInst _inst []
 653         = return ([],False)
 654 substInst inst@(EqInst {tci_left = pattern, tci_right = target}) (i@(EqInst {tci_left = ty1, tci_right = ty2}):is)
 655         = do { (is',changed) <- substInst inst is
 656              ; (coi1,ty1')   <- tcGenericNormalizeFamInst fun ty1
 657              ; (coi2,ty2')   <- tcGenericNormalizeFamInst fun ty2
 658              ; case (coi1,coi2) of
 659                 (IdCo,IdCo) ->
 660                   return (i:is',changed)
 661                 _           ->
 662                   do { gw_co <- eitherEqInst i
 663                                   -- old_co := co1 * new_co * sym co2
 664                                   (\old_covar ->
 665                                    do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty1' ty2')
 666                                       ; let new_co = TyVarTy new_cotv
 667                                       ; let old_coi = coi1 `mkTransCoI` ACo new_co `mkTransCoI` (mkSymCoI coi2)
 668                                       ; writeMetaTyVar old_covar (fromACo old_coi)
 669                                       ; return $ mkWantedCo new_cotv
 670                                       })
 671                                   -- new_co := sym co1 * old_co * co2
 672                                   (\old_co -> return $ mkGivenCo $ fromACo $ (mkSymCoI coi1) `mkTransCoI` ACo old_co `mkTransCoI` coi2)
 673                      ; new_inst <- mkEqInst (EqPred ty1' ty2') gw_co
 674                      ; return (new_inst:is',True)
 675                      }
 676              }
 677         where fun ty = return $ if tcEqType pattern ty then Just (target,coercion) else Nothing
 678
 679               coercion = eitherEqInst inst TyVarTy id
 680 substInst _ _ = panic "TcTyFuns.substInst: not EqInst"
 681
 682 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 683 unifyInsts :: RewriteRule
 684 unifyInsts insts
 685         = do { (insts',changeds) <- mapAndUnzipM unifyInst insts
 686              ; return (concat insts',or changeds)
 687              }
 688
 689         -- (UnifyMeta)
 690         --      g : alpha ~ t
 691         --              >-->
 692         --      alpha := t
 693         --      g     := t
 694         --
 695         --  TOMDO: you should only do this for certain `meta' type variables
 696 unifyInst :: Inst -> TcM ([Inst], Bool)
 697 unifyInst i@(EqInst {tci_left = ty1, tci_right = ty2})
 698         | TyVarTy tv1 <- ty1, isMetaTyVar tv1   = go ty2 tv1
 699         | TyVarTy tv2 <- ty2, isMetaTyVar tv2   = go ty1 tv2
 700         | otherwise                             = return ([i],False)
 701         where go ty tv
 702                 = do { let cotv = fromWantedCo "unifyInst" $ eqInstCoercion i
 703                      ; writeMetaTyVar tv   ty   --      alpha := t
 704                      ; writeMetaTyVar cotv ty   --      g     := t
 705                      ; return ([],True)
 706                      }
 707 unifyInst _ = panic "TcTyFuns.unifyInst: not EqInst"
 708
 709 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 710 occursCheckInsts :: CheckRule
 711 occursCheckInsts insts = mappM_ occursCheckInst insts
 712
 713
 714         -- (OccursCheck)
 715         --      t ~ s[T t]
 716         --              >-->
 717         --      fail
 718         --
 719 occursCheckInst :: Inst -> TcM ()
 720 occursCheckInst (EqInst {tci_left = ty1, tci_right = ty2})
 721         = go ty2
 722         where
 723                 check ty = if ty `tcEqType` ty1
 724                               then occursError
 725                               else go ty
 726
 727                 go (TyConApp con tys)   = if isOpenSynTyCon con then return () else mappM_ check tys
 728                 go (FunTy arg res)      = mappM_ check [arg,res]
 729                 go (AppTy fun arg)      = mappM_ check [fun,arg]
 730                 go _                    = return ()
 731
 732                 occursError             = do { env0 <- tcInitTidyEnv
 733                                              ; let (env1, tidy_ty1)  =  tidyOpenType env0 ty1
 734                                                    (env2, tidy_ty2)  =  tidyOpenType env1 ty2
 735                                                    extra = sep [ppr tidy_ty1, char '~', ppr tidy_ty2]
 736                                              ; failWithTcM (env2, hang msg 2 extra)
 737                                              }
 738                                         where msg = ptext SLIT("Occurs check: cannot construct the infinite type")
 739 occursCheckInst _ = panic "TcTyFuns.occursCheckInst: not eqInst"
 740 \end{code}
 741
 742 Normalises a set of dictionaries relative to a set of given equalities (which
 743 are interpreted as rewrite rules).  We only consider given equalities of the
 744 form
 745
 746   F ts ~ t
 747
 748 where F is a type family.
 749
 750 \begin{code}
 751 substEqInDictInsts :: [Inst]    -- given equalities (used as rewrite rules)
 752                    -> [Inst]    -- dictinaries to be normalised
 753                    -> TcM ([Inst], TcDictBinds)
 754 substEqInDictInsts eq_insts insts
 755   = do { traceTc (text "substEqInDictInst <-" <+> ppr insts)
 756        ; result <- foldlM rewriteWithOneEquality (insts, emptyBag) eq_insts
 757        ; traceTc (text "substEqInDictInst ->" <+> ppr result)
 758        ; return result
 759        }
 760   where
 761       -- (1) Given equality of form 'F ts ~ t': use for rewriting
 762     rewriteWithOneEquality (insts, dictBinds)
 763                            inst@(EqInst {tci_left  = pattern,
 764                                          tci_right = target})
 765       | isOpenSynTyConApp pattern
 766       = do { (insts', moreDictBinds) <- genericNormaliseInsts True {- wanted -}
 767                                                               applyThisEq insts
 768            ; return (insts', dictBinds `unionBags` moreDictBinds)
 769            }
 770       where
 771         applyThisEq = tcGenericNormalizeFamInstPred (return . matchResult)
 772
 773         -- rewrite in case of an exact match
 774         matchResult ty | tcEqType pattern ty = Just (target, eqInstType inst)
 775                        | otherwise           = Nothing
 776
 777       -- (2) Given equality has the wrong form: ignore
 778     rewriteWithOneEquality (insts, dictBinds) _not_a_rewrite_rule
 779       = return (insts, dictBinds)
 780 \end{code}
 781
 782 %************************************************************************
 783 %*                                                                      *
 784         Normalisation of Insts
 785 %*                                                                      *
 786 %************************************************************************
 787
 788 Take a bunch of Insts (not EqInsts), and normalise them wrt the top-level
 789 type-function equations, where
 790
 791         (norm_insts, binds) = normaliseInsts is_wanted insts
 792
 793 If 'is_wanted'
 794   = True,  (binds + norm_insts) defines insts       (wanteds)
 795   = False, (binds + insts)      defines norm_insts  (givens)
 796
 797 \begin{code}
 798 normaliseInsts :: Bool                          -- True <=> wanted insts
 799                -> [Inst]                        -- wanted or given insts
 800                -> TcM ([Inst], TcDictBinds)     -- normalized insts and bindings
 801 normaliseInsts isWanted insts
 802   = genericNormaliseInsts isWanted tcNormalizeFamInstPred insts
 803
 804 genericNormaliseInsts  :: Bool                      -- True <=> wanted insts
 805                        -> (TcPredType -> TcM (CoercionI, TcPredType))
 806                                                     -- how to normalise
 807                        -> [Inst]                    -- wanted or given insts
 808                        -> TcM ([Inst], TcDictBinds) -- normalized insts & binds
 809 genericNormaliseInsts isWanted fun insts
 810   = do { (insts', binds) <- mapAndUnzipM (normaliseOneInst isWanted fun) insts
 811        ; return (insts', unionManyBags binds)
 812        }
 813   where
 814     normaliseOneInst isWanted fun
 815                      dict@(Dict {tci_pred = pred,
 816                                  tci_loc  = loc})
 817       = do { traceTc (text "genericNormaliseInst 1")
 818            ; (coi, pred') <- fun pred
 819            ; traceTc (text "genericNormaliseInst 2")
 820
 821            ; case coi of
 822                IdCo   -> return (dict, emptyBag)
 823                          -- don't use pred' in this case; otherwise, we get
 824                          -- more unfolded closed type synonyms in error messages
 825                ACo co ->
 826                  do { -- an inst for the new pred
 827                     ; dict' <- newDictBndr loc pred'
 828                       -- relate the old inst to the new one
 829                       -- target_dict = source_dict `cast` st_co
 830                     ; let (target_dict, source_dict, st_co)
 831                             | isWanted  = (dict,  dict', mkSymCoercion co)
 832                             | otherwise = (dict', dict,  co)
 833                               -- if isWanted
 834                               --        co :: dict ~ dict'
 835                               --        hence dict = dict' `cast` sym co
 836                               -- else
 837                               --        co :: dict ~ dict'
 838                               --        hence dict' = dict `cast` co
 839                           expr      = HsVar $ instToId source_dict
 840                           cast_expr = HsWrap (WpCo st_co) expr
 841                           rhs       = L (instLocSpan loc) cast_expr
 842                           binds     = mkBind target_dict rhs
 843                       -- return the new inst
 844                     ; return (dict', binds)
 845                     }
 846            }
 847
 848         -- TOMDO: treat other insts appropriately
 849     normaliseOneInst _isWanted _fun inst
 850       = do { inst' <- zonkInst inst
 851            ; return (inst', emptyBag)
 852            }
 853
 854 addBind :: Bag (LHsBind TcId) -> Inst -> LHsExpr TcId -> Bag (LHsBind TcId)
 855 addBind binds inst rhs = binds `unionBags` mkBind inst rhs
 856
 857 mkBind :: Inst -> LHsExpr TcId -> Bag (LHsBind TcId)
 858 mkBind inst rhs = unitBag (L (instSpan inst)
 859                           (VarBind (instToId inst) rhs))
 860 \end{code}