compiler/typecheck/TcTyFuns.lhs

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