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 :: TcType -> TcM (CoercionI, TcType)
  88 tcNormalizeFamInst = tcGenericNormalizeFamInst tcUnfoldSynFamInst
  89
  90 tcNormalizeFamInstPred :: TcPredType -> TcM (CoercionI, TcPredType)
  91 tcNormalizeFamInstPred = tcGenericNormalizeFamInstPred tcUnfoldSynFamInst
  92 \end{code}
  93
  94 Normalise a type relative to the rewrite rule implied by one EqInst.
  95
  96 \begin{code}
  97 tcEqInstNormalizeFamInst :: Inst -> TcType -> TcM (CoercionI, Type)
  98 tcEqInstNormalizeFamInst inst = ASSERT( isEqInst inst )
  99                                 tcGenericNormalizeFamInst matchInst
 100   where
 101     pat = eqInstLeftTy  inst
 102     rhs = eqInstRightTy inst
 103     co  = eitherEqInst  inst TyVarTy id
 104     --
 105     matchInst ty | pat `tcEqType` ty = return $ Just (rhs, co)
 106                  | otherwise         = return $ Nothing
 107 \end{code}
 108
 109 Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
 110 apply the normalisation function gives as the first argument to every TyConApp
 111 and every TyVarTy subterm.
 112
 113         tcGenericNormalizeFamInst fun ty = (co, ty')
 114         then   co : ty ~ ty'
 115
 116 This function is (by way of using smart constructors) careful to ensure that
 117 the returned coercion is exactly IdCo (and not some semantically equivalent,
 118 but syntactically different coercion) whenever (ty' `tcEqType` ty).  This
 119 makes it easy for the caller to determine whether the type changed.  BUT
 120 even if we return IdCo, ty' may be *syntactically* different from ty due to
 121 unfolded closed type synonyms (by way of tcCoreView).  In the interest of
 122 good error messages, callers should discard ty' in favour of ty in this case.
 123
 124 \begin{code}
 125 tcGenericNormalizeFamInst :: (TcType -> TcM (Maybe (TcType, Coercion)))
 126                              -- what to do with type functions and tyvars
 127                            -> TcType                    -- old type
 128                            -> TcM (CoercionI, TcType)   -- (coercion, new type)
 129 tcGenericNormalizeFamInst fun ty
 130   | Just ty' <- tcView ty = tcGenericNormalizeFamInst fun ty'
 131 tcGenericNormalizeFamInst fun (TyConApp tyCon tys)
 132   = do  { (cois, ntys) <- mapAndUnzipM (tcGenericNormalizeFamInst fun) tys
 133         ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
 134         ; maybe_ty_co <- fun (TyConApp tyCon ntys)      -- use normalised args!
 135         ; case maybe_ty_co of
 136             -- a matching family instance exists
 137             Just (ty', co) ->
 138               do { let first_coi = mkTransCoI tycon_coi (ACo co)
 139                  ; (rest_coi, nty) <- tcGenericNormalizeFamInst fun ty'
 140                  ; let fix_coi = mkTransCoI first_coi rest_coi
 141                  ; return (fix_coi, nty)
 142                  }
 143             -- no matching family instance exists
 144             -- we do not do anything
 145             Nothing -> return (tycon_coi, TyConApp tyCon ntys)
 146         }
 147 tcGenericNormalizeFamInst fun (AppTy ty1 ty2)
 148   = do  { (coi1,nty1) <- tcGenericNormalizeFamInst fun ty1
 149         ; (coi2,nty2) <- tcGenericNormalizeFamInst fun ty2
 150         ; return (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2)
 151         }
 152 tcGenericNormalizeFamInst fun (FunTy ty1 ty2)
 153   = do  { (coi1,nty1) <- tcGenericNormalizeFamInst fun ty1
 154         ; (coi2,nty2) <- tcGenericNormalizeFamInst fun ty2
 155         ; return (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2)
 156         }
 157 tcGenericNormalizeFamInst fun (ForAllTy tyvar ty1)
 158   = do  { (coi,nty1) <- tcGenericNormalizeFamInst fun ty1
 159         ; return (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
 160         }
 161 tcGenericNormalizeFamInst fun (NoteTy note ty1)
 162   = do  { (coi,nty1) <- tcGenericNormalizeFamInst fun ty1
 163         ; return (mkNoteTyCoI note coi,NoteTy note nty1)
 164         }
 165 tcGenericNormalizeFamInst fun ty@(TyVarTy tv)
 166   | isTcTyVar tv
 167   = do  { traceTc (text "tcGenericNormalizeFamInst" <+> ppr ty)
 168         ; res <- lookupTcTyVar tv
 169         ; case res of
 170             DoneTv _ ->
 171               do { maybe_ty' <- fun ty
 172                  ; case maybe_ty' of
 173                      Nothing         -> return (IdCo, ty)
 174                      Just (ty', co1) ->
 175                        do { (coi2, ty'') <- tcGenericNormalizeFamInst fun ty'
 176                           ; return (ACo co1 `mkTransCoI` coi2, ty'')
 177                           }
 178                  }
 179             IndirectTv ty' -> tcGenericNormalizeFamInst fun ty'
 180         }
 181   | otherwise
 182   = return (IdCo, ty)
 183 tcGenericNormalizeFamInst fun (PredTy predty)
 184   = do  { (coi, pred') <- tcGenericNormalizeFamInstPred fun predty
 185         ; return (coi, PredTy pred') }
 186
 187 ---------------------------------
 188 tcGenericNormalizeFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
 189                               -> TcPredType
 190                               -> TcM (CoercionI, TcPredType)
 191
 192 tcGenericNormalizeFamInstPred fun (ClassP cls tys)
 193   = do { (cois, tys')<- mapAndUnzipM (tcGenericNormalizeFamInst fun) tys
 194        ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
 195        }
 196 tcGenericNormalizeFamInstPred fun (IParam ipn ty)
 197   = do { (coi, ty') <- tcGenericNormalizeFamInst fun ty
 198        ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
 199        }
 200 tcGenericNormalizeFamInstPred fun (EqPred ty1 ty2)
 201   = do { (coi1, ty1') <- tcGenericNormalizeFamInst fun ty1
 202        ; (coi2, ty2') <- tcGenericNormalizeFamInst fun ty2
 203        ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
 204 \end{code}
 205
 206
 207 %************************************************************************
 208 %*                                                                      *
 209 \section{Normalisation of Given Dictionaries}
 210 %*                                                                      *
 211 %************************************************************************
 212
 213 \begin{code}
 214 normaliseGivenDicts, normaliseWantedDicts
 215         :: [Inst]               -- given equations
 216         -> [Inst]               -- dictionaries
 217         -> TcM ([Inst],TcDictBinds)
 218
 219 normaliseGivenDicts  eqs dicts = normalise_dicts eqs dicts False
 220 normaliseWantedDicts eqs dicts = normalise_dicts eqs dicts True
 221
 222 normalise_dicts
 223         :: [Inst]       -- given equations
 224         -> [Inst]       -- dictionaries
 225         -> Bool         -- True <=> the dicts are wanted
 226                         -- Fals <=> they are given
 227         -> TcM ([Inst],TcDictBinds)
 228 normalise_dicts given_eqs dicts is_wanted
 229   = do  { traceTc $ text "normaliseGivenDicts <-" <+> ppr dicts <+>
 230                     text "with" <+> ppr given_eqs
 231         ; (dicts0, binds0)  <- normaliseInsts is_wanted dicts
 232         ; (dicts1, binds1)  <- substEqInDictInsts given_eqs dicts0
 233         ; let binds01 = binds0 `unionBags` binds1
 234         ; if isEmptyBag binds1
 235           then return (dicts1, binds01)
 236           else do { (dicts2, binds2) <- normaliseGivenDicts given_eqs dicts1
 237                   ; return (dicts2, binds01 `unionBags` binds2) } }
 238 \end{code}
 239
 240
 241 %************************************************************************
 242 %*                                                                      *
 243 \section{Normalisation of wanteds constraints}
 244 %*                                                                      *
 245 %************************************************************************
 246
 247 \begin{code}
 248 normaliseWanteds :: [Inst] -> TcM [Inst]
 249 normaliseWanteds insts
 250   = do { traceTc (text "normaliseWanteds <-" <+> ppr insts)
 251        ; result <- liftM fst $ rewriteToFixedPoint Nothing
 252                      [ ("(Occurs)",  noChange  $ occursCheckInsts)
 253                      , ("(ZONK)",    dontRerun $ zonkInsts)
 254                      , ("(TRIVIAL)", trivialInsts)
 255                      -- no `swapInsts'; it messes up error messages and should
 256                      -- not be necessary -=chak
 257                      , ("(DECOMP)",  decompInsts)
 258                      , ("(TOP)",     topInsts)
 259                      , ("(SUBST)",   substInsts)
 260                      , ("(UNIFY)",   unifyInsts)
 261                      ] insts
 262        ; traceTc (text "normaliseWanteds ->" <+> ppr result)
 263        ; return result
 264        }
 265 \end{code}
 266
 267
 268 %************************************************************************
 269 %*                                                                      *
 270 \section{Normalisation of givens constraints}
 271 %*                                                                      *
 272 %************************************************************************
 273
 274 \begin{code}
 275 normaliseGivens :: [Inst] -> TcM ([Inst], TcM ())
 276 normaliseGivens givens
 277  = do { traceTc (text "normaliseGivens <-" <+> ppr givens)
 278       ; (result, deSkolem) <-
 279           rewriteToFixedPoint (Just ("(SkolemOccurs)", skolemOccurs))
 280             [ ("(Occurs)",  noChange  $ occursCheckInsts)
 281             , ("(ZONK)",    dontRerun $ zonkInsts)
 282             , ("(TRIVIAL)", trivialInsts)
 283             , ("(SWAP)",    swapInsts)
 284             , ("(DECOMP)",  decompInsts)
 285             , ("(TOP)",     topInsts)
 286             , ("(SUBST)",   substInsts)
 287             ] givens
 288       ; traceTc (text "normaliseGivens ->" <+> ppr result)
 289       ; return (result, deSkolem)
 290       }
 291 \end{code}
 292
 293
 294 This is an (attempt at, yet unproven, an) *unflattened* version of
 295 the SubstL-Ev completion rule.
 296
 297 The above rule is essential to catch non-terminating
 298 rules that cannot be oriented properly, like
 299
 300      F a ~ [G (F a)]
 301  or even
 302      a ~ [G a]
 303
 304 The left-to-right orientiation is not suitable because it does not
 305 terminate.
 306 The right-to-left orientation is not suitable because it
 307 does not have a type-function on the left. This is undesirable because
 308 it would hide information. E.g. assume
 309         instance C [x]
 310 then rewriting C [G (F a)] to C (F a) is bad because we cannot now
 311 see that the C [x] instance applies.
 312
 313 The rule also caters for badly-oriented rules of the form:
 314      F a ~ G (F a)
 315 for which other solutions are possible, but this one will do too.
 316
 317 It's behavior is:
 318   co : ty1 ~ ty2{F ty1}
 319      >-->
 320   co         : ty1 ~ ty2{b}
 321   sym (F co) : F ty2{b} ~ b
 322         where b is a fresh skolem variable
 323
 324 We also return an action (b := ty1) which is used to eliminate b
 325 after the dust of normalisation with the completed rewrite system
 326 has settled.
 327
 328 A subtle point of this transformation is that both coercions in the results
 329 are strictly speaking incorrect.  However, they are correct again after the
 330 action {B := ty1} has removed the skolem again.  This happens immediately
 331 after constraint entailment has been checked; ie, code outside of the
 332 simplification and entailment checking framework will never see these
 333 temporarily incorrect coercions.
 334
 335 NB: We perform this transformation for multiple occurences of ty1 under one
 336     or multiple family applications on the left-hand side at once (ie, the
 337     rule doesn't need to be applied multiple times at a single inst).  As a
 338     result we can get two or more insts back.
 339
 340 \begin{code}
 341 skolemOccurs :: PrecondRule
 342 skolemOccurs insts
 343   = do { (instss, undoSkolems) <- mapAndUnzipM oneSkolemOccurs insts
 344        ; return (concat instss, sequence_ undoSkolems)
 345        }
 346   where
 347     oneSkolemOccurs inst
 348       | null tysToLiftOut
 349       = return ([inst], return ())
 350       | otherwise
 351       = do { skTvs <- mapM (newMetaTyVar TauTv . typeKind) tysToLiftOut
 352            ; let skTvs_tysTLO   = zip skTvs tysToLiftOut
 353                  insertSkolems = return . replace skTvs_tysTLO
 354            ; (_, ty2') <- tcGenericNormalizeFamInst insertSkolems ty2
 355            ; inst' <- mkEqInst (EqPred ty1 ty2') co
 356            ; (insts, undoSk) <- mapAndUnzipM (mkSkolemInst inst') skTvs_tysTLO
 357            ; return (inst':insts, sequence_ undoSk)
 358            }
 359       where
 360         ty1 = eqInstLeftTy   inst
 361         ty2 = eqInstRightTy  inst
 362         co  = eqInstCoercion inst
 363
 364         -- all subtypes that are (1) type family instances and (2) contain the
 365         -- lhs type as part of the type arguments of the type family constructor
 366         tysToLiftOut = ASSERT( isEqInst inst )
 367                        [mkTyConApp tc tys | (tc, tys) <- tyFamInsts ty2
 368                                           , any (ty1 `tcPartOfType`) tys]
 369
 370         replace :: [(TcTyVar, Type)] -> Type -> Maybe (Type, Coercion)
 371         replace []                   _  = Nothing
 372         replace ((skTv, tyTLO):rest) ty
 373           | tyTLO `tcEqType` ty         = Just (mkTyVarTy skTv, undefined)
 374           | otherwise                   = replace rest ty
 375
 376         -- create the EqInst for the equality determining the skolem and a
 377         -- TcM action undoing the skolem introduction
 378         mkSkolemInst inst' (skTv, tyTLO)
 379           = do { (co, tyLiftedOut) <- tcEqInstNormalizeFamInst inst' tyTLO
 380                ; inst <- mkEqInst (EqPred tyLiftedOut (mkTyVarTy skTv))
 381                                   (mkGivenCo $ mkSymCoercion (fromACo co))
 382                ; return (inst, writeMetaTyVar skTv tyTLO)
 383                }
 384 \end{code}
 385
 386
 387 %************************************************************************
 388 %*                                                                      *
 389 \section{Solving of wanted constraints with respect to a given set}
 390 %*                                                                      *
 391 %************************************************************************
 392
 393 \begin{code}
 394 solveWanteds :: [Inst]          -- givens
 395              -> [Inst]          -- wanteds
 396              -> TcM [Inst]      -- irreducible wanteds
 397 solveWanteds givens wanteds
 398   = do { traceTc $ text "solveWanteds <-" <+> ppr wanteds <+> text "with" <+>
 399                    ppr givens
 400        ; result <- liftM fst $ rewriteToFixedPoint Nothing
 401                      [ ("(Occurs)",  noChange $ occursCheckInsts)
 402                      , ("(TRIVIAL)", trivialInsts)
 403                      , ("(DECOMP)",  decompInsts)
 404                      , ("(TOP)",     topInsts)
 405                      , ("(GIVEN)",   givenInsts givens)
 406                      , ("(UNIFY)",   unifyInsts)
 407                      ] wanteds
 408        ; traceTc (text "solveWanteds ->" <+> ppr result)
 409        ; return result
 410        }
 411   where
 412     -- Use `substInst' with every given on all the wanteds.
 413     givenInsts :: [Inst] -> [Inst] -> TcM ([Inst],Bool)
 414     givenInsts []     wanteds = return (wanteds,False)
 415     givenInsts (g:gs) wanteds
 416       = do { (wanteds1, changed1) <- givenInsts gs wanteds
 417            ; (wanteds2, changed2) <- substInst g wanteds1
 418            ; return (wanteds2, changed1 || changed2)
 419            }
 420 \end{code}
 421
 422
 423 %************************************************************************
 424 %*                                                                      *
 425 \section{Normalisation rules and iterative rule application}
 426 %*                                                                      *
 427 %************************************************************************
 428
 429 We have four kinds of normalising rewrite rules:
 430
 431 (1) Normalisation rules that rewrite a set of insts and return a flag indicating
 432     whether any changes occurred during rewriting that necessitate re-running
 433     the current rule set.
 434
 435 (2) Precondition rules that rewrite a set of insts and return a monadic action
 436     that reverts the effect of preconditioning.
 437
 438 (3) Idempotent normalisation rules that never require re-running the rule set.
 439
 440 (4) Checking rule that does not alter the set of insts.
 441
 442 \begin{code}
 443 type RewriteRule     = [Inst] -> TcM ([Inst], Bool)   -- rewrite, maybe re-run
 444 type PrecondRule     = [Inst] -> TcM ([Inst], TcM ()) -- rewrite, revertable
 445 type IdemRewriteRule = [Inst] -> TcM [Inst]           -- rewrite, don't re-run
 446 type CheckRule       = [Inst] -> TcM ()               -- check
 447
 448 type NamedRule       = (String, RewriteRule)          -- rule with description
 449 type NamedPreRule    = (String, PrecondRule)          -- precond with desc
 450 \end{code}
 451
 452 Templates lifting idempotent and checking rules to full rules (which can be put
 453 into a rule set).
 454
 455 \begin{code}
 456 dontRerun :: IdemRewriteRule -> RewriteRule
 457 dontRerun rule insts = liftM addFalse $ rule insts
 458   where
 459     addFalse x = (x, False)
 460
 461 noChange :: CheckRule -> RewriteRule
 462 noChange rule insts = rule insts >> return (insts, False)
 463 \end{code}
 464
 465 The following function applies a set of rewrite rules until a fixed point is
 466 reached; i.e., none of the `RewriteRule's require re-running the rule set.
 467 Optionally, there may be a pre-conditing rule that is applied before any other
 468 rules are applied and before the rule set is re-run.
 469
 470 The result is the set of rewritten (i.e., normalised) insts and, in case of a
 471 pre-conditing rule, a monadic action that reverts the effects of
 472 pre-conditioning - specifically, this is removing introduced skolems.
 473
 474 \begin{code}
 475 rewriteToFixedPoint :: Maybe NamedPreRule   -- optional preconditioning rule
 476                     -> [NamedRule]          -- rule set
 477                     -> [Inst]               -- insts to rewrite
 478                     -> TcM ([Inst], TcM ())
 479 rewriteToFixedPoint precondRule rules insts
 480   = completeRewrite (return ()) precondRule insts
 481   where
 482     completeRewrite :: TcM () -> Maybe NamedPreRule -> [Inst]
 483                     -> TcM ([Inst], TcM ())
 484     completeRewrite dePrecond (Just (precondName, precond)) insts
 485       = do { (insts', dePrecond') <- precond insts
 486            ; traceTc $ text precondName <+> ppr insts'
 487            ; tryRules (dePrecond >> dePrecond') rules insts'
 488            }
 489     completeRewrite dePrecond Nothing insts
 490       = tryRules dePrecond rules insts
 491
 492     tryRules dePrecond _                    []    = return ([]   , dePrecond)
 493     tryRules dePrecond []                   insts = return (insts, dePrecond)
 494     tryRules dePrecond ((name, rule):rules) insts
 495       = do { (insts', rerun) <- rule insts
 496            ; traceTc $ text name <+> ppr insts'
 497            ; if rerun then completeRewrite dePrecond precondRule insts'
 498                       else tryRules dePrecond rules insts'
 499            }
 500 \end{code}
 501
 502
 503 %************************************************************************
 504 %*                                                                      *
 505 \section{Different forms of Inst rewritings}
 506 %*                                                                      *
 507 %************************************************************************
 508
 509 Rewrite schemata applied by way of eq_rewrite and friends.
 510
 511 \begin{code}
 512
 513         -- (Trivial)
 514         --      g1 : t ~ t
 515         --              >-->
 516         --      g1 := t
 517         --
 518 trivialInsts :: RewriteRule
 519 trivialInsts []
 520         = return ([],False)
 521 trivialInsts (i@(EqInst {}):is)
 522         = do { (is',changed)<- trivialInsts is
 523              ; if tcEqType ty1 ty2
 524                   then do { eitherEqInst i
 525                                 (\covar -> writeMetaTyVar covar ty1)
 526                                 (\_     -> return ())
 527                           ; return (is',True)
 528                           }
 529                   else return (i:is',changed)
 530              }
 531         where
 532            ty1 = eqInstLeftTy i
 533            ty2 = eqInstRightTy i
 534 trivialInsts _ = panic "TcTyFuns.trivialInsts: not EqInst"
 535
 536 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 537 swapInsts :: RewriteRule
 538 -- All the inputs and outputs are equalities
 539 swapInsts insts
 540   = do { (insts', changeds) <- mapAndUnzipM swapInst insts
 541        ; return (insts', or changeds)
 542        }
 543
 544         -- (Swap)
 545         --      g1 : c ~ F d
 546         --              >-->
 547         --      g2 : F d ~ c
 548         --      g1 := sym g2
 549         --              where c isn't a function call
 550         --  and
 551         --
 552         --      g1 : c ~ a
 553         --              >-->
 554         --      g2 : a ~ c
 555         --      g1 := sym g2
 556         --              where c isn't a function call or other variable
 557 swapInst :: Inst -> TcM (Inst, Bool)
 558 swapInst i@(EqInst {})
 559         = go ty1 ty2
 560         where
 561               ty1 = eqInstLeftTy i
 562               ty2 = eqInstRightTy i
 563               go ty1 ty2                | Just ty1' <- tcView ty1
 564                                         = go ty1' ty2
 565               go ty1 ty2                | Just ty2' <- tcView ty2
 566                                         = go ty1 ty2'
 567               go (TyConApp tyCon _) _   | isOpenSynTyCon tyCon
 568                                         = return (i,False)
 569                 -- we should swap!
 570               go ty1 ty2@(TyConApp tyCon _)
 571                                         | isOpenSynTyCon tyCon
 572                                         = actual_swap ty1 ty2
 573               go ty1@(TyConApp _ _) ty2@(TyVarTy _)
 574                                         = actual_swap ty1 ty2
 575               go _ _                    = return (i,False)
 576
 577               actual_swap ty1 ty2 = do { wg_co <- eitherEqInst i
 578                                                           -- old_co := sym new_co
 579                                                           (\old_covar ->
 580                                                            do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty2 ty1)
 581                                                               ; let new_co = TyVarTy new_cotv
 582                                                               ; writeMetaTyVar old_covar (mkCoercion symCoercionTyCon [new_co])
 583                                                               ; return $ mkWantedCo new_cotv
 584                                                               })
 585                                                           -- new_co := sym old_co
 586                                                           (\old_co -> return $ mkGivenCo $ mkCoercion symCoercionTyCon [old_co])
 587                                              ; new_inst <- mkEqInst (EqPred ty2 ty1) wg_co
 588                                              ; return (new_inst,True)
 589                                              }
 590 swapInst _ = panic "TcTyFuns.swapInst: not EqInst"
 591
 592 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 593 decompInsts :: RewriteRule
 594 decompInsts insts = do { (insts,bs) <- mapAndUnzipM decompInst insts
 595                        ; return (concat insts,or bs)
 596                        }
 597
 598         -- (Decomp)
 599         --      g1 : T cs ~ T ds
 600         --              >-->
 601         --      g21 : c1 ~ d1, ..., g2n : cn ~ dn
 602         --      g1 := T g2s
 603         --
 604         --  Works also for the case where T is actually an application of a
 605         --  type family constructor to a set of types, provided the
 606         --  applications on both sides of the ~ are identical;
 607         --  see also Note [OpenSynTyCon app] in TcUnify
 608         --
 609 decompInst :: Inst -> TcM ([Inst],Bool)
 610 decompInst i@(EqInst {})
 611   = go ty1 ty2
 612   where
 613     ty1 = eqInstLeftTy i
 614     ty2 = eqInstRightTy i
 615     go ty1 ty2
 616       | Just ty1' <- tcView ty1 = go ty1' ty2
 617       | Just ty2' <- tcView ty2 = go ty1 ty2'
 618
 619     go ty1@(TyConApp con1 tys1) ty2@(TyConApp con2 tys2)
 620       | con1 == con2 && identicalHead
 621       = do { cos <- eitherEqInst i
 622                       -- old_co := Con1 cos
 623                       (\old_covar ->
 624                         do { cotvs <- zipWithM (\t1 t2 ->
 625                                                 newMetaTyVar TauTv
 626                                                              (mkCoKind t1 t2))
 627                                                tys1 tys2
 628                            ; let cos = map TyVarTy cotvs
 629                            ; writeMetaTyVar old_covar (TyConApp con1 cos)
 630                            ; return $ map mkWantedCo cotvs
 631                            })
 632                       -- co_i := Con_i old_co
 633                       (\old_co -> return $
 634                                     map mkGivenCo $
 635                                         mkRightCoercions (length tys1) old_co)
 636            ; insts <- zipWithM mkEqInst (zipWith EqPred tys1 tys2) cos
 637            ; traceTc (text "decomp identicalHead" <+> ppr insts)
 638            ; return (insts, not $ null insts)
 639            }
 640       | con1 /= con2 && not (isOpenSynTyCon con1 || isOpenSynTyCon con2)
 641         -- not matching data constructors (of any flavour) are bad news
 642       = do { env0 <- tcInitTidyEnv
 643            ; let (env1, tidy_ty1) = tidyOpenType env0 ty1
 644                  (env2, tidy_ty2) = tidyOpenType env1 ty2
 645                  extra            = sep [ppr tidy_ty1, char '~', ppr tidy_ty2]
 646                  msg              =
 647                    ptext SLIT("Unsolvable equality constraint:")
 648            ; failWithTcM (env2, hang msg 2 extra)
 649            }
 650       where
 651         n             = tyConArity con1
 652         (idxTys1, _)  = splitAt n tys1
 653         (idxTys2, _)  = splitAt n tys2
 654         identicalHead = not (isOpenSynTyCon con1) ||
 655                         idxTys1 `tcEqTypes` idxTys2
 656
 657     go _ _ = return ([i], False)
 658 decompInst _ = panic "TcTyFuns.decompInst: not EqInst"
 659
 660 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 661 topInsts :: RewriteRule
 662 topInsts insts
 663         =  do { (insts,bs) <- mapAndUnzipM topInst insts
 664               ; return (insts,or bs)
 665               }
 666
 667         -- (Top)
 668         --      g1 : t ~ s
 669         --              >--> co1 :: t ~ t' / co2 :: s ~ s'
 670         --      g2 : t' ~ s'
 671         --      g1 := co1 * g2 * sym co2
 672 topInst :: Inst -> TcM (Inst,Bool)
 673 topInst i@(EqInst {})
 674         = do { (coi1,ty1') <- tcNormalizeFamInst ty1
 675              ; (coi2,ty2') <- tcNormalizeFamInst ty2
 676              ; case (coi1,coi2) of
 677                 (IdCo,IdCo) ->
 678                   return (i,False)
 679                 _           ->
 680                  do { wg_co <- eitherEqInst i
 681                                  -- old_co = co1 * new_co * sym co2
 682                                  (\old_covar ->
 683                                   do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty1 ty2)
 684                                      ; let new_co = TyVarTy new_cotv
 685                                      ; let old_coi = coi1 `mkTransCoI` ACo new_co `mkTransCoI` (mkSymCoI coi2)
 686                                      ; writeMetaTyVar old_covar (fromACo old_coi)
 687                                      ; return $ mkWantedCo new_cotv
 688                                      })
 689                                  -- new_co = sym co1 * old_co * co2
 690                                  (\old_co -> return $ mkGivenCo $ fromACo $ mkSymCoI coi1 `mkTransCoI` ACo old_co `mkTransCoI` coi2)
 691                     ; new_inst <- mkEqInst (EqPred ty1' ty2') wg_co
 692                     ; return (new_inst,True)
 693                     }
 694              }
 695         where
 696               ty1 = eqInstLeftTy i
 697               ty2 = eqInstRightTy i
 698 topInst _ = panic "TcTyFuns.topInsts: not EqInst"
 699
 700 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 701 substInsts :: RewriteRule
 702 substInsts insts = substInstsWorker insts []
 703
 704 substInstsWorker :: [Inst] -> [Inst] -> TcM ([Inst],Bool)
 705 substInstsWorker [] acc
 706         = return (acc,False)
 707 substInstsWorker (i:is) acc
 708         | (TyConApp con _) <- tci_left i, isOpenSynTyCon con
 709         = do { (is',change) <- substInst i (acc ++ is)
 710              ; if change
 711                   then return ((i:is'),True)
 712                   else substInstsWorker is (i:acc)
 713              }
 714         | (TyVarTy _) <- tci_left i
 715         = do { (is',change) <- substInst i (acc ++ is)
 716              ; if change
 717                   then return ((i:is'),True)
 718                   else substInstsWorker is (i:acc)
 719              }
 720         | otherwise
 721         = substInstsWorker is (i:acc)
 722
 723         -- (Subst)
 724         --      g : F c ~ t,
 725         --      forall g1 : s1{F c} ~ s2{F c}
 726         --              >-->
 727         --      g2 : s1{t} ~ s2{t}
 728         --      g1 := s1{g} * g2  * sym s2{g}           <=>     g2 := sym s1{g} * g1 * s2{g}
 729 substInst :: Inst -> [Inst] -> TcM ([Inst], Bool)
 730 substInst _inst [] = return ([],False)
 731 substInst inst (i@(EqInst {tci_left = ty1, tci_right = ty2}):is)
 732         = do { (is',changed) <- substInst inst is
 733              ; (coi1,ty1')   <- normalise ty1
 734              ; (coi2,ty2')   <- normalise ty2
 735              ; case (coi1,coi2) of
 736                 (IdCo,IdCo) ->
 737                   return (i:is',changed)
 738                 _           ->
 739                   do { gw_co <- eitherEqInst i
 740                                   -- old_co := co1 * new_co * sym co2
 741                                   (\old_covar ->
 742                                    do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty1' ty2')
 743                                       ; let new_co = TyVarTy new_cotv
 744                                       ; let old_coi = coi1 `mkTransCoI` ACo new_co `mkTransCoI` (mkSymCoI coi2)
 745                                       ; writeMetaTyVar old_covar (fromACo old_coi)
 746                                       ; return $ mkWantedCo new_cotv
 747                                       })
 748                                   -- new_co := sym co1 * old_co * co2
 749                                   (\old_co -> return $ mkGivenCo $ fromACo $ (mkSymCoI coi1) `mkTransCoI` ACo old_co `mkTransCoI` coi2)
 750                      ; new_inst <- mkEqInst (EqPred ty1' ty2') gw_co
 751                      ; return (new_inst:is',True)
 752                      }
 753              }
 754         where
 755           normalise = tcEqInstNormalizeFamInst inst
 756 substInst _ _ = panic "TcTyFuns.substInst: not EqInst"
 757
 758 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 759 unifyInsts :: RewriteRule
 760 unifyInsts insts
 761         = do { (insts',changeds) <- mapAndUnzipM unifyInst insts
 762              ; return (concat insts',or changeds)
 763              }
 764
 765         -- (UnifyMeta)
 766         --      g : alpha ~ t
 767         --              >-->
 768         --      alpha := t
 769         --      g     := t
 770         --
 771         --  TOMDO: you should only do this for certain `meta' type variables
 772 unifyInst :: Inst -> TcM ([Inst], Bool)
 773 unifyInst i@(EqInst {tci_left = ty1, tci_right = ty2})
 774         | TyVarTy tv1 <- ty1, isMetaTyVar tv1   = go ty2 tv1
 775         | TyVarTy tv2 <- ty2, isMetaTyVar tv2   = go ty1 tv2
 776         | otherwise                             = return ([i],False)
 777         where go ty tv
 778                 = do { let cotv = fromWantedCo "unifyInst" $ eqInstCoercion i
 779                      ; writeMetaTyVar tv   ty   --      alpha := t
 780                      ; writeMetaTyVar cotv ty   --      g     := t
 781                      ; return ([],True)
 782                      }
 783 unifyInst _ = panic "TcTyFuns.unifyInst: not EqInst"
 784
 785 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 786 occursCheckInsts :: CheckRule
 787 occursCheckInsts insts = mappM_ occursCheckInst insts
 788
 789
 790         -- (OccursCheck)
 791         --      t ~ s[T t]
 792         --              >-->
 793         --      fail
 794         --
 795 occursCheckInst :: Inst -> TcM ()
 796 occursCheckInst (EqInst {tci_left = ty1, tci_right = ty2})
 797         = go ty2
 798         where
 799                 check ty = if ty `tcEqType` ty1
 800                               then occursError
 801                               else go ty
 802
 803                 go (TyConApp con tys)   = if isOpenSynTyCon con then return () else mappM_ check tys
 804                 go (FunTy arg res)      = mappM_ check [arg,res]
 805                 go (AppTy fun arg)      = mappM_ check [fun,arg]
 806                 go _                    = return ()
 807
 808                 occursError             = do { env0 <- tcInitTidyEnv
 809                                              ; let (env1, tidy_ty1)  =  tidyOpenType env0 ty1
 810                                                    (env2, tidy_ty2)  =  tidyOpenType env1 ty2
 811                                                    extra = sep [ppr tidy_ty1, char '~', ppr tidy_ty2]
 812                                              ; failWithTcM (env2, hang msg 2 extra)
 813                                              }
 814                                         where msg = ptext SLIT("Occurs check: cannot construct the infinite type")
 815 occursCheckInst _ = panic "TcTyFuns.occursCheckInst: not eqInst"
 816 \end{code}
 817
 818 Normalises a set of dictionaries relative to a set of given equalities (which
 819 are interpreted as rewrite rules).  We only consider given equalities of the
 820 form
 821
 822   F ts ~ t
 823
 824 where F is a type family.
 825
 826 \begin{code}
 827 substEqInDictInsts :: [Inst]    -- given equalities (used as rewrite rules)
 828                    -> [Inst]    -- dictinaries to be normalised
 829                    -> TcM ([Inst], TcDictBinds)
 830 substEqInDictInsts eq_insts insts
 831   = do { traceTc (text "substEqInDictInst <-" <+> ppr insts)
 832        ; result <- foldlM rewriteWithOneEquality (insts, emptyBag) eq_insts
 833        ; traceTc (text "substEqInDictInst ->" <+> ppr result)
 834        ; return result
 835        }
 836   where
 837       -- (1) Given equality of form 'F ts ~ t': use for rewriting
 838     rewriteWithOneEquality (insts, dictBinds)
 839                            inst@(EqInst {tci_left  = pattern,
 840                                          tci_right = target})
 841       | isOpenSynTyConApp pattern
 842       = do { (insts', moreDictBinds) <- genericNormaliseInsts True {- wanted -}
 843                                                               applyThisEq insts
 844            ; return (insts', dictBinds `unionBags` moreDictBinds)
 845            }
 846       where
 847         applyThisEq = tcGenericNormalizeFamInstPred (return . matchResult)
 848
 849         -- rewrite in case of an exact match
 850         matchResult ty | tcEqType pattern ty = Just (target, eqInstType inst)
 851                        | otherwise           = Nothing
 852
 853       -- (2) Given equality has the wrong form: ignore
 854     rewriteWithOneEquality (insts, dictBinds) _not_a_rewrite_rule
 855       = return (insts, dictBinds)
 856 \end{code}
 857
 858 %************************************************************************
 859 %*                                                                      *
 860         Normalisation of Insts
 861 %*                                                                      *
 862 %************************************************************************
 863
 864 Take a bunch of Insts (not EqInsts), and normalise them wrt the top-level
 865 type-function equations, where
 866
 867         (norm_insts, binds) = normaliseInsts is_wanted insts
 868
 869 If 'is_wanted'
 870   = True,  (binds + norm_insts) defines insts       (wanteds)
 871   = False, (binds + insts)      defines norm_insts  (givens)
 872
 873 \begin{code}
 874 normaliseInsts :: Bool                          -- True <=> wanted insts
 875                -> [Inst]                        -- wanted or given insts
 876                -> TcM ([Inst], TcDictBinds)     -- normalized insts and bindings
 877 normaliseInsts isWanted insts
 878   = genericNormaliseInsts isWanted tcNormalizeFamInstPred insts
 879
 880 genericNormaliseInsts  :: Bool                      -- True <=> wanted insts
 881                        -> (TcPredType -> TcM (CoercionI, TcPredType))
 882                                                     -- how to normalise
 883                        -> [Inst]                    -- wanted or given insts
 884                        -> TcM ([Inst], TcDictBinds) -- normalized insts & binds
 885 genericNormaliseInsts isWanted fun insts
 886   = do { (insts', binds) <- mapAndUnzipM (normaliseOneInst isWanted fun) insts
 887        ; return (insts', unionManyBags binds)
 888        }
 889   where
 890     normaliseOneInst isWanted fun
 891                      dict@(Dict {tci_pred = pred,
 892                                  tci_loc  = loc})
 893       = do { traceTc (text "genericNormaliseInst 1")
 894            ; (coi, pred') <- fun pred
 895            ; traceTc (text "genericNormaliseInst 2")
 896
 897            ; case coi of
 898                IdCo   -> return (dict, emptyBag)
 899                          -- don't use pred' in this case; otherwise, we get
 900                          -- more unfolded closed type synonyms in error messages
 901                ACo co ->
 902                  do { -- an inst for the new pred
 903                     ; dict' <- newDictBndr loc pred'
 904                       -- relate the old inst to the new one
 905                       -- target_dict = source_dict `cast` st_co
 906                     ; let (target_dict, source_dict, st_co)
 907                             | isWanted  = (dict,  dict', mkSymCoercion co)
 908                             | otherwise = (dict', dict,  co)
 909                               -- if isWanted
 910                               --        co :: dict ~ dict'
 911                               --        hence dict = dict' `cast` sym co
 912                               -- else
 913                               --        co :: dict ~ dict'
 914                               --        hence dict' = dict `cast` co
 915                           expr      = HsVar $ instToId source_dict
 916                           cast_expr = HsWrap (WpCo st_co) expr
 917                           rhs       = L (instLocSpan loc) cast_expr
 918                           binds     = mkBind target_dict rhs
 919                       -- return the new inst
 920                     ; return (dict', binds)
 921                     }
 922            }
 923
 924         -- TOMDO: treat other insts appropriately
 925     normaliseOneInst _isWanted _fun inst
 926       = do { inst' <- zonkInst inst
 927            ; return (inst', emptyBag)
 928            }
 929
 930 addBind :: Bag (LHsBind TcId) -> Inst -> LHsExpr TcId -> Bag (LHsBind TcId)
 931 addBind binds inst rhs = binds `unionBags` mkBind inst rhs
 932
 933 mkBind :: Inst -> LHsExpr TcId -> Bag (LHsBind TcId)
 934 mkBind inst rhs = unitBag (L (instSpan inst)
 935                           (VarBind (instToId inst) rhs))
 936 \end{code}