compiler/typecheck/TcTyFuns.lhs

   1 Normalisation of type terms relative to type instances as well as
   2 normalisation and entailment checking of equality constraints.
   3
   4 \begin{code}
   5 module TcTyFuns (
   6   -- type normalisation wrt to toplevel equalities only
   7   tcNormaliseFamInst,
   8
   9   -- instance normalisation wrt to equalities
  10   tcReduceEqs,
  11
  12   -- errors
  13   misMatchMsg, failWithMisMatch,
  14
  15 ) where
  16
  17
  18 #include "HsVersions.h"
  19
  20 --friends
  21 import TcRnMonad
  22 import TcEnv
  23 import Inst
  24 import TcType
  25 import TcMType
  26
  27 -- GHC
  28 import Coercion
  29 import Type
  30 import TypeRep  ( Type(..) )
  31 import TyCon
  32 import HsSyn
  33 import VarEnv
  34 import VarSet
  35 import Var
  36 import Name
  37 import Bag
  38 import Outputable
  39 import SrcLoc   ( Located(..) )
  40 import Maybes
  41 import FastString
  42
  43 -- standard
  44 import Data.List
  45 import Control.Monad
  46 \end{code}
  47
  48
  49 %************************************************************************
  50 %*                                                                      *
  51                 Normalisation of types wrt toplevel equality schemata
  52 %*                                                                      *
  53 %************************************************************************
  54
  55 Unfold a single synonym family instance and yield the witnessing coercion.
  56 Return 'Nothing' if the given type is either not synonym family instance
  57 or is a synonym family instance that has no matching instance declaration.
  58 (Applies only if the type family application is outermost.)
  59
  60 For example, if we have
  61
  62   :Co:R42T a :: T [a] ~ :R42T a
  63
  64 then 'T [Int]' unfolds to (:R42T Int, :Co:R42T Int).
  65
  66 \begin{code}
  67 tcUnfoldSynFamInst :: Type -> TcM (Maybe (Type, Coercion))
  68 tcUnfoldSynFamInst (TyConApp tycon tys)
  69   | not (isOpenSynTyCon tycon)     -- unfold *only* _synonym_ family instances
  70   = return Nothing
  71   | otherwise
  72   = do { -- The TyCon might be over-saturated, but that's ok for tcLookupFamInst
  73        ; maybeFamInst <- tcLookupFamInst tycon tys
  74        ; case maybeFamInst of
  75            Nothing                -> return Nothing
  76            Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc rep_tys,
  77                                                     mkTyConApp coe_tc rep_tys)
  78              where
  79                coe_tc = expectJust "TcTyFuns.tcUnfoldSynFamInst"
  80                                    (tyConFamilyCoercion_maybe rep_tc)
  81        }
  82 tcUnfoldSynFamInst _other = return Nothing
  83 \end{code}
  84
  85 Normalise 'Type's and 'PredType's by unfolding type family applications where
  86 possible (ie, we treat family instances as a TRS).  Also zonk meta variables.
  87
  88         tcNormaliseFamInst ty = (co, ty')
  89         then   co : ty ~ ty'
  90
  91 \begin{code}
  92 -- |Normalise the given type as far as possible with toplevel equalities.
  93 -- This results in a coercion witnessing the type equality, in addition to the
  94 -- normalised type.
  95 --
  96 tcNormaliseFamInst :: TcType -> TcM (CoercionI, TcType)
  97 tcNormaliseFamInst = tcGenericNormaliseFamInst tcUnfoldSynFamInst
  98 \end{code}
  99
 100 Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
 101 apply the normalisation function gives as the first argument to every TyConApp
 102 and every TyVarTy subterm.
 103
 104         tcGenericNormaliseFamInst fun ty = (co, ty')
 105         then   co : ty ~ ty'
 106
 107 This function is (by way of using smart constructors) careful to ensure that
 108 the returned coercion is exactly IdCo (and not some semantically equivalent,
 109 but syntactically different coercion) whenever (ty' `tcEqType` ty).  This
 110 makes it easy for the caller to determine whether the type changed.  BUT
 111 even if we return IdCo, ty' may be *syntactically* different from ty due to
 112 unfolded closed type synonyms (by way of tcCoreView).  In the interest of
 113 good error messages, callers should discard ty' in favour of ty in this case.
 114
 115 \begin{code}
 116 tcGenericNormaliseFamInst :: (TcType -> TcM (Maybe (TcType, Coercion)))
 117                              -- what to do with type functions and tyvars
 118                            -> TcType                    -- old type
 119                            -> TcM (CoercionI, TcType)   -- (coercion, new type)
 120 tcGenericNormaliseFamInst fun ty
 121   | Just ty' <- tcView ty = tcGenericNormaliseFamInst fun ty'
 122 tcGenericNormaliseFamInst fun (TyConApp tyCon tys)
 123   = do  { (cois, ntys) <- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
 124         ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
 125         ; maybe_ty_co <- fun (mkTyConApp tyCon ntys)     -- use normalised args!
 126         ; case maybe_ty_co of
 127             -- a matching family instance exists
 128             Just (ty', co) ->
 129               do { let first_coi = mkTransCoI tycon_coi (ACo co)
 130                  ; (rest_coi, nty) <- tcGenericNormaliseFamInst fun ty'
 131                  ; let fix_coi = mkTransCoI first_coi rest_coi
 132                  ; return (fix_coi, nty)
 133                  }
 134             -- no matching family instance exists
 135             -- we do not do anything
 136             Nothing -> return (tycon_coi, mkTyConApp tyCon ntys)
 137         }
 138 tcGenericNormaliseFamInst fun (AppTy ty1 ty2)
 139   = do  { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
 140         ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
 141         ; return (mkAppTyCoI nty1 coi1 nty2 coi2, mkAppTy nty1 nty2)
 142         }
 143 tcGenericNormaliseFamInst fun (FunTy ty1 ty2)
 144   = do  { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
 145         ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
 146         ; return (mkFunTyCoI nty1 coi1 nty2 coi2, mkFunTy nty1 nty2)
 147         }
 148 tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1)
 149   = do  { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
 150         ; return (mkForAllTyCoI tyvar coi, mkForAllTy tyvar nty1)
 151         }
 152 tcGenericNormaliseFamInst fun ty@(TyVarTy tv)
 153   | isTcTyVar tv
 154   = do  { traceTc (text "tcGenericNormaliseFamInst" <+> ppr ty)
 155         ; res <- lookupTcTyVar tv
 156         ; case res of
 157             DoneTv _ ->
 158               do { maybe_ty' <- fun ty
 159                  ; case maybe_ty' of
 160                      Nothing         -> return (IdCo, ty)
 161                      Just (ty', co1) ->
 162                        do { (coi2, ty'') <- tcGenericNormaliseFamInst fun ty'
 163                           ; return (ACo co1 `mkTransCoI` coi2, ty'')
 164                           }
 165                  }
 166             IndirectTv ty' -> tcGenericNormaliseFamInst fun ty'
 167         }
 168   | otherwise
 169   = return (IdCo, ty)
 170 tcGenericNormaliseFamInst fun (PredTy predty)
 171   = do  { (coi, pred') <- tcGenericNormaliseFamInstPred fun predty
 172         ; return (coi, PredTy pred') }
 173
 174 ---------------------------------
 175 tcGenericNormaliseFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
 176                               -> TcPredType
 177                               -> TcM (CoercionI, TcPredType)
 178
 179 tcGenericNormaliseFamInstPred fun (ClassP cls tys)
 180   = do { (cois, tys')<- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
 181        ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
 182        }
 183 tcGenericNormaliseFamInstPred fun (IParam ipn ty)
 184   = do { (coi, ty') <- tcGenericNormaliseFamInst fun ty
 185        ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
 186        }
 187 tcGenericNormaliseFamInstPred fun (EqPred ty1 ty2)
 188   = do { (coi1, ty1') <- tcGenericNormaliseFamInst fun ty1
 189        ; (coi2, ty2') <- tcGenericNormaliseFamInst fun ty2
 190        ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
 191 \end{code}
 192
 193
 194 %************************************************************************
 195 %*                                                                      *
 196                 Normalisation of instances wrt to equalities
 197 %*                                                                      *
 198 %************************************************************************
 199
 200 Given a set of given, local constraints and a set of wanted constraints,
 201 simplify the wanted equalities as far as possible and normalise both local and
 202 wanted dictionaries with respect to the equalities.
 203
 204 In addition to the normalised local dictionaries and simplified wanteds, the
 205 function yields bindings for instantiated meta variables (due to solving
 206 equality constraints) and dictionary bindings (due to simplifying class
 207 constraints).  The bag of type variable bindings only contains bindings for
 208 non-local variables - i.e., type variables other than those newly created by
 209 the present function.  Consequently, type improvement took place iff the bag
 210 of bindings contains any bindings for proper type variables (not just covars).
 211 The solver does not instantiate any non-local variables; i.e., the bindings
 212 must be executed by the caller.
 213
 214 All incoming constraints are assumed to be zonked already.  All outgoing
 215 constraints will be zonked again.
 216
 217 NB: The solver only has local effects that cannot be observed from outside.
 218     In particular, it can be executed twice on the same constraint set with
 219     the same result (modulo generated variables names).
 220
 221 \begin{code}
 222 tcReduceEqs :: [Inst]             -- locals
 223             -> [Inst]             -- wanteds
 224             -> TcM ([Inst],       -- normalised locals (w/o equalities)
 225                     [Inst],       -- normalised wanteds (including equalities)
 226                     TcTyVarBinds, -- bindings for meta type variables
 227                     TcDictBinds)  -- bindings for all simplified dictionaries
 228 tcReduceEqs locals wanteds
 229   = do { ((locals, wanteds, dictBinds), tyBinds) <- getTcTyVarBinds $
 230            do { let (local_eqs  , local_dicts)   = partition isEqInst locals
 231                     (wanteds_eqs, wanteds_dicts) = partition isEqInst wanteds
 232               ; eqCfg1 <- normaliseEqs (local_eqs ++ wanteds_eqs)
 233               ; eqCfg2 <- normaliseDicts False local_dicts
 234               ; eqCfg3 <- normaliseDicts True  wanteds_dicts
 235               ; eqCfg <- propagateEqs (eqCfg1 `unionEqConfig`
 236                                        eqCfg2 `unionEqConfig`
 237                                        eqCfg3)
 238               ; finaliseEqsAndDicts freeFlexibles eqCfg
 239               }
 240          -- execute type bindings of skolem flexibles...
 241        ; tyBinds_pruned <- pruneTyBinds tyBinds freeFlexibles
 242          -- ...and zonk the constraints to propagate the bindings
 243        ; locals_z  <- zonkInsts locals
 244        ; wanteds_z <- zonkInsts wanteds
 245        ; return (locals_z, wanteds_z, tyBinds_pruned, dictBinds)
 246        }
 247    where
 248      -- unification variables that appear in the environment and may not be
 249      -- instantiated - this includes coercion variables
 250      freeFlexibles = tcTyVarsOfInsts locals `unionVarSet`
 251                      tcTyVarsOfInsts wanteds
 252
 253      pruneTyBinds tybinds freeFlexibles
 254        = do { let tybinds'                      = bagToList tybinds
 255                   (skolem_tybinds, env_tybinds) = partition isSkolem tybinds'
 256             ; execTcTyVarBinds (listToBag skolem_tybinds)
 257             ; return $ listToBag env_tybinds
 258             }
 259        where
 260          isSkolem (TcTyVarBind tv _ ) = not (tv `elemVarSet` freeFlexibles)
 261 \end{code}
 262
 263
 264 %************************************************************************
 265 %*                                                                      *
 266                 Equality Configurations
 267 %*                                                                      *
 268 %************************************************************************
 269
 270 We maintain normalised equalities together with the skolems introduced as
 271 intermediates during flattening of equalities as well as
 272
 273 \begin{code}
 274 -- |Configuration of normalised equalities used during solving.
 275 --
 276 data EqConfig = EqConfig { eqs     :: [RewriteInst]     -- all equalities
 277                          , locals  :: [Inst]            -- given dicts
 278                          , wanteds :: [Inst]            -- wanted dicts
 279                          , binds   :: TcDictBinds       -- bindings
 280                          }
 281
 282 addEq :: EqConfig -> RewriteInst -> EqConfig
 283 addEq eqCfg eq = eqCfg {eqs = eq : eqs eqCfg}
 284
 285 unionEqConfig :: EqConfig -> EqConfig -> EqConfig
 286 unionEqConfig eqc1 eqc2 = EqConfig
 287                           { eqs     = eqs eqc1 ++ eqs eqc2
 288                           , locals  = locals eqc1 ++ locals eqc2
 289                           , wanteds = wanteds eqc1 ++ wanteds eqc2
 290                           , binds   = binds eqc1 `unionBags` binds eqc2
 291                           }
 292
 293 emptyEqConfig :: EqConfig
 294 emptyEqConfig = EqConfig
 295                 { eqs     = []
 296                 , locals  = []
 297                 , wanteds = []
 298                 , binds   = emptyBag
 299                 }
 300
 301 instance Outputable EqConfig where
 302   ppr (EqConfig {eqs = eqs, locals = locals, wanteds = wanteds, binds = binds})
 303     = vcat [ppr eqs, ppr locals, ppr wanteds, ppr binds]
 304 \end{code}
 305
 306 The set of operations on an equality configuration.  We obtain the initialise
 307 configuration by normalisation ('normaliseEqs'), solve the equalities by
 308 propagation ('propagateEqs'), and eventually finalise the configuration when
 309 no further propoagation is possible.
 310
 311 \begin{code}
 312 -- |Turn a set of equalities into an equality configuration for solving.
 313 --
 314 -- Precondition: The Insts are zonked.
 315 --
 316 normaliseEqs :: [Inst] -> TcM EqConfig
 317 normaliseEqs eqs
 318   = do { WARNM2( anyM wantedEqInstIsUnsolved eqs, ppr eqs )
 319        ; traceTc $ ptext (sLit "Entering normaliseEqs")
 320
 321        ; eqss <- mapM normEqInst eqs
 322        ; return $ emptyEqConfig { eqs = concat eqss }
 323        }
 324
 325 -- |Flatten the type arguments of all dictionaries, returning the result as a
 326 -- equality configuration.  The dictionaries go into the 'wanted' component if
 327 -- the second argument is 'True'.
 328 --
 329 -- Precondition: The Insts are zonked.
 330 --
 331 normaliseDicts :: Bool -> [Inst] -> TcM EqConfig
 332 normaliseDicts isWanted insts
 333   = do { traceTc $ hang (ptext (sLit "Entering normaliseDicts") <+>
 334                          ptext (if isWanted then sLit "[Wanted] for"
 335                                             else sLit "[Local] for"))
 336                      4 (ppr insts)
 337
 338        ; (insts', eqss, bindss) <- mapAndUnzip3M (normDict isWanted) insts
 339
 340        ; traceTc $ hang (ptext (sLit "normaliseDicts returns"))
 341                      4 (ppr insts' $$ ppr eqss)
 342        ; return $ emptyEqConfig { eqs     = concat eqss
 343                                 , locals  = if isWanted then [] else insts'
 344                                 , wanteds = if isWanted then insts' else []
 345                                 , binds   = unionManyBags bindss
 346                                 }
 347        }
 348
 349 -- |Solves the equalities as far as possible by applying propagation rules.
 350 --
 351 propagateEqs :: EqConfig -> TcM EqConfig
 352 propagateEqs eqCfg@(EqConfig {eqs = todoEqs})
 353   = do { traceTc $ hang (ptext (sLit "Entering propagateEqs:"))
 354                      4 (ppr eqCfg)
 355
 356        ; propagate todoEqs (eqCfg {eqs = []})
 357        }
 358
 359 -- |Finalise a set of equalities and associated dictionaries after
 360 -- propagation.  The first returned set of instances are the locals (without
 361 -- equalities) and the second set are all residual wanteds, including
 362 -- equalities.  In addition, we return all generated dictionary bindings.
 363 --
 364 finaliseEqsAndDicts :: TcTyVarSet -> EqConfig
 365                     -> TcM ([Inst], [Inst], TcDictBinds)
 366 finaliseEqsAndDicts freeFlexibles (EqConfig { eqs     = eqs
 367                                             , locals  = locals
 368                                             , wanteds = wanteds
 369                                             , binds   = binds
 370                                             })
 371   = do { traceTc $ ptext (sLit "finaliseEqsAndDicts")
 372
 373        ; (eqs', subst_binds, locals', wanteds')
 374            <- substitute eqs locals wanteds checkingMode freeFlexibles
 375        ; eqs'' <- bindAndExtract eqs' checkingMode freeFlexibles
 376        ; let final_binds = subst_binds `unionBags` binds
 377
 378          -- Assert that all cotvs of wanted equalities are still unfilled, and
 379          -- zonk all final insts, to make any improvement visible
 380        ; ASSERTM2( allM wantedEqInstIsUnsolved eqs'', ppr eqs'' )
 381        ; zonked_locals  <- zonkInsts locals'
 382        ; zonked_wanteds <- zonkInsts (eqs'' ++ wanteds')
 383        ; return (zonked_locals, zonked_wanteds, final_binds)
 384        }
 385   where
 386     checkingMode = length eqs > length wanteds || not (null locals)
 387                      -- no local equalities or dicts => checking mode
 388 \end{code}
 389
 390
 391 %************************************************************************
 392 %*                                                                      *
 393                 Normalisation of equalities
 394 %*                                                                      *
 395 %************************************************************************
 396
 397 A normal equality is a properly oriented equality with associated coercion
 398 that contains at most one family equality (in its left-hand side) is oriented
 399 such that it may be used as a rewrite rule.  It has one of the following two
 400 forms:
 401
 402 (1) co :: F t1..tn ~ t  (family equalities)
 403 (2) co :: x ~ t         (variable equalities)
 404
 405 Variable equalities fall again in two classes:
 406
 407 (2a) co :: x ~ t, where t is *not* a variable, or
 408 (2b) co :: x ~ y, where x > y.
 409
 410 The types t, t1, ..., tn may not contain any occurrences of synonym
 411 families.  Moreover, in Forms (2) & (3), the left-hand side may not occur in
 412 the right-hand side, and the relation x > y is an (nearly) arbitrary, but
 413 total order on type variables.  The only restriction that we impose on that
 414 order is that for x > y, we are happy to instantiate x with y taking into
 415 account kinds, signature skolems etc (cf, TcUnify.uUnfilledVars).
 416
 417 \begin{code}
 418 data RewriteInst
 419   = RewriteVar  -- Form (2) above
 420     { rwi_var     :: TyVar    -- may be rigid or flexible
 421     , rwi_right   :: TcType   -- contains no synonym family applications
 422     , rwi_co      :: EqInstCo -- the wanted or given coercion
 423     , rwi_loc     :: InstLoc
 424     , rwi_name    :: Name     -- no semantic significance (cf. TcRnTypes.EqInst)
 425     , rwi_swapped :: Bool     -- swapped orientation of original EqInst
 426     }
 427   | RewriteFam  -- Forms (1) above
 428     { rwi_fam     :: TyCon    -- synonym family tycon
 429     , rwi_args    :: [Type]   -- contain no synonym family applications
 430     , rwi_right   :: TcType   -- contains no synonym family applications
 431     , rwi_co      :: EqInstCo -- the wanted or given coercion
 432     , rwi_loc     :: InstLoc
 433     , rwi_name    :: Name     -- no semantic significance (cf. TcRnTypes.EqInst)
 434     , rwi_swapped :: Bool     -- swapped orientation of original EqInst
 435     }
 436
 437 isWantedRewriteInst :: RewriteInst -> Bool
 438 isWantedRewriteInst = isWantedCo . rwi_co
 439
 440 isRewriteVar :: RewriteInst -> Bool
 441 isRewriteVar (RewriteVar {}) = True
 442 isRewriteVar _               = False
 443
 444 tyVarsOfRewriteInst :: RewriteInst -> TyVarSet
 445 tyVarsOfRewriteInst (RewriteVar {rwi_var = tv, rwi_right = ty})
 446   = unitVarSet tv `unionVarSet` tyVarsOfType ty
 447 tyVarsOfRewriteInst (RewriteFam {rwi_args = args, rwi_right = ty})
 448   = tyVarsOfTypes args `unionVarSet` tyVarsOfType ty
 449
 450 rewriteInstToInst :: RewriteInst -> TcM Inst
 451 rewriteInstToInst eq@(RewriteVar {rwi_var = tv})
 452   = deriveEqInst eq (mkTyVarTy tv) (rwi_right eq) (rwi_co eq)
 453 rewriteInstToInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
 454   = deriveEqInst eq (mkTyConApp fam args) (rwi_right eq) (rwi_co eq)
 455
 456 -- Derive an EqInst based from a RewriteInst, possibly swapping the types
 457 -- around.
 458 --
 459 deriveEqInst :: RewriteInst -> TcType -> TcType -> EqInstCo -> TcM Inst
 460 deriveEqInst rewrite ty1 ty2 co
 461   = do { co_adjusted <- if not swapped then return co
 462                                        else mkSymEqInstCo co (ty2, ty1)
 463        ; return $ EqInst
 464                   { tci_left  = left
 465                   , tci_right = right
 466                   , tci_co    = co_adjusted
 467                   , tci_loc   = rwi_loc rewrite
 468                   , tci_name  = rwi_name rewrite
 469                   }
 470        }
 471   where
 472     swapped       = rwi_swapped rewrite
 473     (left, right) = if not swapped then (ty1, ty2) else (ty2, ty1)
 474
 475 instance Outputable RewriteInst where
 476   ppr (RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = rhs, rwi_co =co})
 477     = hsep [ pprEqInstCo co <+> text "::"
 478            , ppr (mkTyConApp fam args)
 479            , text "~>"
 480            , ppr rhs
 481            ]
 482   ppr (RewriteVar {rwi_var = tv, rwi_right = rhs, rwi_co =co})
 483     = hsep [ pprEqInstCo co <+> text "::"
 484            , ppr tv
 485            , text "~>"
 486            , ppr rhs
 487            ]
 488
 489 pprEqInstCo :: EqInstCo -> SDoc
 490 pprEqInstCo (Left cotv) = ptext (sLit "Wanted") <+> ppr cotv
 491 pprEqInstCo (Right co)  = ptext (sLit "Local") <+> ppr co
 492 \end{code}
 493
 494 The following functions turn an arbitrary equality into a set of normal
 495 equalities.  This implements the WFlat and LFlat rules of the paper in one
 496 sweep.  However, we use flexible variables for both locals and wanteds, and
 497 avoid to carry around the unflattening substitution \Sigma (for locals) by
 498 already updating the skolems for locals with the family application that they
 499 represent - i.e., they will turn into that family application on the next
 500 zonking (which only happens after finalisation).
 501
 502 In a corresponding manner, normDict normalises class dictionaries by
 503 extracting any synonym family applications and generation appropriate normal
 504 equalities.
 505
 506 Whenever we encounter a loopy equality (of the form a ~ T .. (F ...a...) ...),
 507 we drop that equality and raise an error if it is a wanted or a warning if it
 508 is a local.
 509
 510 \begin{code}
 511 normEqInst :: Inst -> TcM [RewriteInst]
 512 -- Normalise one equality.
 513 normEqInst inst
 514   = ASSERT( isEqInst inst )
 515     do { traceTc $ ptext (sLit "normEqInst of ") <+>
 516                    pprEqInstCo co <+> text "::" <+>
 517                    ppr ty1 <+> text "~" <+> ppr ty2
 518        ; res <- go ty1 ty2 co
 519
 520        ; traceTc $ ptext (sLit "normEqInst returns") <+> ppr res
 521        ; return res
 522        }
 523   where
 524     (ty1, ty2) = eqInstTys inst
 525     co         = eqInstCoercion inst
 526
 527       -- look through synonyms
 528     go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
 529     go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
 530
 531       -- left-to-right rule with type family head
 532     go ty1@(TyConApp con args) ty2 co
 533       | isOpenSynTyConApp ty1           -- only if not oversaturated
 534       = mkRewriteFam False con args ty2 co
 535
 536       -- right-to-left rule with type family head
 537     go ty1 ty2@(TyConApp con args) co
 538       | isOpenSynTyConApp ty2           -- only if not oversaturated
 539       = do { co' <- mkSymEqInstCo co (ty2, ty1)
 540            ; mkRewriteFam True con args ty1 co'
 541            }
 542
 543       -- no outermost family
 544     go ty1 ty2 co
 545       = do { (ty1', co1, ty1_eqs) <- flattenType inst ty1
 546            ; (ty2', co2, ty2_eqs) <- flattenType inst ty2
 547            ; let ty12_eqs  = ty1_eqs ++ ty2_eqs
 548                  sym_co2   = mkSymCoercion co2
 549                  eqTys     = (ty1', ty2')
 550            ; (co', ty12_eqs') <- adjustCoercions co co1 sym_co2 eqTys ty12_eqs
 551            ; eqs <- checkOrientation ty1' ty2' co' inst
 552            ; if isLoopyEquality eqs ty12_eqs'
 553              then do { if isWantedCo (tci_co inst)
 554                        then
 555                           addErrCtxt (ptext (sLit "Rejecting loopy equality")) $
 556                             eqInstMisMatch inst
 557                        else
 558                          warnDroppingLoopyEquality ty1 ty2
 559                      ; return ([])                 -- drop the equality
 560                      }
 561              else
 562                return (eqs ++ ty12_eqs')
 563            }
 564
 565     mkRewriteFam swapped con args ty2 co
 566       = do { (args', cargs, args_eqss) <- mapAndUnzip3M (flattenType inst) args
 567            ; (ty2', co2, ty2_eqs) <- flattenType inst ty2
 568            ; let co1       = mkTyConApp con cargs
 569                  sym_co2   = mkSymCoercion co2
 570                  all_eqs   = concat args_eqss ++ ty2_eqs
 571                  eqTys     = (mkTyConApp con args', ty2')
 572            ; (co', all_eqs') <- adjustCoercions co co1 sym_co2 eqTys all_eqs
 573            ; let thisRewriteFam = RewriteFam
 574                                   { rwi_fam     = con
 575                                   , rwi_args    = args'
 576                                   , rwi_right   = ty2'
 577                                   , rwi_co      = co'
 578                                   , rwi_loc     = tci_loc inst
 579                                   , rwi_name    = tci_name inst
 580                                   , rwi_swapped = swapped
 581                                   }
 582            ; return $ thisRewriteFam : all_eqs'
 583            }
 584
 585     -- If the original equality has the form a ~ T .. (F ...a...) ..., we will
 586     -- have a variable equality with 'a' on the lhs as the first equality.
 587     -- Then, check whether 'a' occurs in the lhs of any family equality
 588     -- generated by flattening.
 589     isLoopyEquality (RewriteVar {rwi_var = tv}:_) eqs = any inRewriteFam eqs
 590       where
 591         inRewriteFam (RewriteFam {rwi_args = args})
 592           = tv `elemVarSet` tyVarsOfTypes args
 593         inRewriteFam _ = False
 594     isLoopyEquality _ _ = False
 595
 596 normDict :: Bool -> Inst -> TcM (Inst, [RewriteInst], TcDictBinds)
 597 -- Normalise one dictionary or IP constraint.
 598 normDict isWanted inst@(Dict {tci_pred = ClassP clas args})
 599   = do { (args', cargs, args_eqss) <- mapAndUnzip3M (flattenType inst) args
 600        ; let rewriteCo = PredTy $ ClassP clas cargs
 601              eqs       = concat args_eqss
 602              pred'     = ClassP clas args'
 603        ; if null eqs
 604          then  -- don't generate a binding if there is nothing to flatten
 605            return (inst, [], emptyBag)
 606          else do {
 607        ; (inst', bind) <- mkDictBind inst isWanted rewriteCo pred'
 608        ; eqs' <- if isWanted then return eqs else mapM wantedToLocal eqs
 609        ; return (inst', eqs', bind)
 610        }}
 611 normDict _isWanted inst
 612   = return (inst, [], emptyBag)
 613 -- !!!TODO: Still need to normalise IP constraints.
 614
 615 checkOrientation :: Type -> Type -> EqInstCo -> Inst -> TcM [RewriteInst]
 616 -- Performs the occurs check, decomposition, and proper orientation
 617 -- (returns a singleton, or an empty list in case of a trivial equality)
 618 -- NB: We cannot assume that the two types already have outermost type
 619 --     synonyms expanded due to the recursion in the case of type applications.
 620 checkOrientation ty1 ty2 co inst
 621   = go ty1 ty2
 622   where
 623       -- look through synonyms
 624     go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
 625     go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
 626
 627       -- identical types => trivial
 628     go ty1 ty2
 629       | ty1 `tcEqType` ty2
 630       = do { mkIdEqInstCo co ty1
 631            ; return []
 632            }
 633
 634       -- two tvs (distinct tvs, due to previous equation)
 635     go ty1@(TyVarTy tv1) ty2@(TyVarTy tv2)
 636       = do { isBigger <- tv1 `tvIsBigger` tv2
 637            ; if isBigger                                      -- left greater
 638                then mkRewriteVar False tv1 ty2 co             --   => unchanged
 639                else do { co' <- mkSymEqInstCo co (ty2, ty1)   -- right greater
 640                        ; mkRewriteVar True tv2 ty1 co'        --   => swap
 641                        }
 642            }
 643
 644       -- only lhs is a tv => unchanged
 645     go ty1@(TyVarTy tv1) ty2
 646       | ty1 `tcPartOfType` ty2      -- occurs check!
 647       = occurCheckErr ty1 ty2
 648       | otherwise
 649       = mkRewriteVar False tv1 ty2 co
 650
 651       -- only rhs is a tv => swap
 652     go ty1 ty2@(TyVarTy tv2)
 653       | ty2 `tcPartOfType` ty1      -- occurs check!
 654       = occurCheckErr ty2 ty1
 655       | otherwise
 656       = do { co' <- mkSymEqInstCo co (ty2, ty1)
 657            ; mkRewriteVar True tv2 ty1 co'
 658            }
 659
 660       -- data type constructor application => decompose
 661       -- NB: Special cased for efficiency - could be handled as type application
 662     go (TyConApp con1 args1) (TyConApp con2 args2)
 663       |  con1 == con2
 664       && isInjectiveTyCon con1   -- don't match family synonym apps
 665       = do { co_args <- mkTyConEqInstCo co con1 (zip args1 args2)
 666            ; eqss <- zipWith3M (\ty1 ty2 co -> checkOrientation ty1 ty2 co inst)
 667                      args1 args2 co_args
 668            ; return $ concat eqss
 669            }
 670
 671       -- function type => decompose
 672       -- NB: Special cased for efficiency - could be handled as type application
 673     go (FunTy ty1_l ty1_r) (FunTy ty2_l ty2_r)
 674       = do { (co_l, co_r) <- mkFunEqInstCo co (ty1_l, ty2_l) (ty1_r, ty2_r)
 675            ; eqs_l <- checkOrientation ty1_l ty2_l co_l inst
 676            ; eqs_r <- checkOrientation ty1_r ty2_r co_r inst
 677            ; return $ eqs_l ++ eqs_r
 678            }
 679
 680       -- type applications => decompose
 681     go ty1 ty2
 682       | Just (ty1_l, ty1_r) <- repSplitAppTy_maybe ty1   -- won't split fam apps
 683       , Just (ty2_l, ty2_r) <- repSplitAppTy_maybe ty2
 684       = do { (co_l, co_r) <- mkAppEqInstCo co (ty1_l, ty2_l) (ty1_r, ty2_r)
 685            ; eqs_l <- checkOrientation ty1_l ty2_l co_l inst
 686            ; eqs_r <- checkOrientation ty1_r ty2_r co_r inst
 687            ; return $ eqs_l ++ eqs_r
 688            }
 689
 690       -- inconsistency => type error
 691     go ty1 ty2
 692       = ASSERT( (not . isForAllTy $ ty1) && (not . isForAllTy $ ty2) )
 693         eqInstMisMatch inst
 694
 695     mkRewriteVar swapped tv ty co = return [RewriteVar
 696                                             { rwi_var     = tv
 697                                             , rwi_right   = ty
 698                                             , rwi_co      = co
 699                                             , rwi_loc     = tci_loc inst
 700                                             , rwi_name    = tci_name inst
 701                                             , rwi_swapped = swapped
 702                                             }]
 703
 704     -- if tv1 `tvIsBigger` tv2, we make a rewrite rule tv1 ~> tv2
 705     tvIsBigger :: TcTyVar -> TcTyVar -> TcM Bool
 706     tvIsBigger tv1 tv2
 707       = isBigger tv1 (tcTyVarDetails tv1) tv2 (tcTyVarDetails tv2)
 708       where
 709         isBigger tv1 (SkolemTv _)     tv2 (SkolemTv _)
 710           = return $ tv1 > tv2
 711         isBigger _   (MetaTv _ _)     _   (SkolemTv _)
 712           = return True
 713         isBigger _   (SkolemTv _)     _   (MetaTv _ _)
 714           = return False
 715         isBigger tv1 (MetaTv info1 _) tv2 (MetaTv info2 _)
 716           -- meta variable meets meta variable
 717           -- => be clever about which of the two to update
 718           --   (from TcUnify.uUnfilledVars minus boxy stuff)
 719           = case (info1, info2) of
 720               -- Avoid SigTvs if poss
 721               (SigTv _, SigTv _)             -> return $ tv1 > tv2
 722               (SigTv _, _      ) | k1_sub_k2 -> return False
 723               (_,       SigTv _) | k2_sub_k1 -> return True
 724
 725               (_, _)
 726                 | k1_sub_k2 &&
 727                   k2_sub_k1
 728                   -> case (nicer_to_update tv1, nicer_to_update tv2) of
 729                        (True, False) -> return True
 730                        (False, True) -> return False
 731                        _             -> return $ tv1 > tv2
 732                 | k1_sub_k2    -> return False
 733                 | k2_sub_k1    -> return True
 734                 | otherwise    -> kind_err >> return True
 735               -- Update the variable with least kind info
 736               -- See notes on type inference in Kind.lhs
 737               -- The "nicer to" part only applies if the two kinds are the same,
 738               -- so we can choose which to do.
 739           where
 740             kind_err = addErrCtxtM (unifyKindCtxt False tv1 (mkTyVarTy tv2)) $
 741                        unifyKindMisMatch k1 k2
 742
 743             k1 = tyVarKind tv1
 744             k2 = tyVarKind tv2
 745             k1_sub_k2 = k1 `isSubKind` k2
 746             k2_sub_k1 = k2 `isSubKind` k1
 747
 748             nicer_to_update tv = isSystemName (Var.varName tv)
 749                 -- Try to update sys-y type variables in preference to ones
 750                 -- gotten (say) by instantiating a polymorphic function with
 751                 -- a user-written type sig
 752
 753 flattenType :: Inst     -- context to get location  & name
 754             -> Type     -- the type to flatten
 755             -> TcM (Type,           -- the flattened type
 756                     Coercion,       -- coercion witness of flattening wanteds
 757                     [RewriteInst])  -- extra equalities
 758 -- Removes all family synonyms from a type by moving them into extra equalities
 759 flattenType inst ty = go ty
 760   where
 761       -- look through synonyms
 762     go ty | Just ty' <- tcView ty
 763       = do { (ty_flat, co, eqs) <- go ty'
 764            ; if null eqs
 765              then     -- unchanged, keep the old type with folded synonyms
 766                return (ty, ty, [])
 767              else
 768                return (ty_flat, co, eqs)
 769            }
 770
 771       -- type variable => nothing to do
 772     go ty@(TyVarTy _)
 773       = return (ty, ty, [])
 774
 775       -- type family application & family arity matches number of args
 776       -- => flatten to "gamma :: F t1'..tn' ~ alpha" (alpha & gamma fresh)
 777     go ty@(TyConApp con args)
 778       | isOpenSynTyConApp ty   -- only if not oversaturated
 779       = do { (args', cargs, args_eqss) <- mapAndUnzip3M go args
 780            ; alpha <- newFlexiTyVar (typeKind ty)
 781            ; let alphaTy = mkTyVarTy alpha
 782            ; cotv <- newMetaCoVar (mkTyConApp con args') alphaTy
 783            ; let thisRewriteFam = RewriteFam
 784                                   { rwi_fam     = con
 785                                   , rwi_args    = args'
 786                                   , rwi_right   = alphaTy
 787                                   , rwi_co      = mkWantedCo cotv
 788                                   , rwi_loc     = tci_loc inst
 789                                   , rwi_name    = tci_name inst
 790                                   , rwi_swapped = True
 791                                   }
 792            ; return (alphaTy,
 793                      mkTyConApp con cargs `mkTransCoercion` mkTyVarTy cotv,
 794                      thisRewriteFam : concat args_eqss)
 795            }
 796
 797       -- datatype constructor application => flatten subtypes
 798       -- NB: Special cased for efficiency - could be handled as type application
 799     go ty@(TyConApp con args)
 800       | not (isOpenSynTyCon con)   -- don't match oversaturated family apps
 801       = do { (args', cargs, args_eqss) <- mapAndUnzip3M go args
 802            ; let args_eqs = concat args_eqss
 803            ; if null args_eqs
 804              then     -- unchanged, keep the old type with folded synonyms
 805                return (ty, ty, [])
 806              else
 807                return (mkTyConApp con args',
 808                        mkTyConApp con cargs,
 809                        args_eqs)
 810            }
 811
 812       -- function type => flatten subtypes
 813       -- NB: Special cased for efficiency - could be handled as type application
 814     go ty@(FunTy ty_l ty_r)
 815       = do { (ty_l', co_l, eqs_l) <- go ty_l
 816            ; (ty_r', co_r, eqs_r) <- go ty_r
 817            ; if null eqs_l && null eqs_r
 818              then     -- unchanged, keep the old type with folded synonyms
 819                return (ty, ty, [])
 820              else
 821                return (mkFunTy ty_l' ty_r',
 822                        mkFunTy co_l co_r,
 823                        eqs_l ++ eqs_r)
 824            }
 825
 826       -- type application => flatten subtypes
 827     go ty
 828       | Just (ty_l, ty_r) <- repSplitAppTy_maybe ty
 829                              -- need to use the smart split as ty may be an
 830                              -- oversaturated family application
 831       = do { (ty_l', co_l, eqs_l) <- go ty_l
 832            ; (ty_r', co_r, eqs_r) <- go ty_r
 833            ; if null eqs_l && null eqs_r
 834              then     -- unchanged, keep the old type with folded synonyms
 835                return (ty, ty, [])
 836              else
 837                return (mkAppTy ty_l' ty_r',
 838                        mkAppTy co_l co_r,
 839                        eqs_l ++ eqs_r)
 840            }
 841
 842       -- forall type => panic if the body contains a type family
 843       -- !!!TODO: As long as the family does not contain a quantified variable
 844       --          we might pull it out, but what if it does contain a quantified
 845       --          variable???
 846     go ty@(ForAllTy _ body)
 847       | null (tyFamInsts body)
 848       = return (ty, ty, [])
 849       | otherwise
 850       = panic "TcTyFuns.flattenType: synonym family in a rank-n type"
 851
 852       -- predicate type => handle like a datatype constructor application
 853     go (PredTy (ClassP cls tys))
 854       = do { (tys', ctys, tys_eqss) <- mapAndUnzip3M go tys
 855            ; let tys_eqs = concat tys_eqss
 856            ; if null tys_eqs
 857              then     -- unchanged, keep the old type with folded synonyms
 858                return (ty, ty, [])
 859              else
 860                return (PredTy (ClassP cls tys'),
 861                        PredTy (ClassP cls ctys),
 862                        tys_eqs)
 863            }
 864
 865       -- implicit parameter => flatten subtype
 866     go ty@(PredTy (IParam ipn ity))
 867       = do { (ity', co, eqs) <- go ity
 868            ; if null eqs
 869              then return (ty, ty, [])
 870              else return (PredTy (IParam ipn ity'),
 871                           PredTy (IParam ipn co),
 872                           eqs)
 873            }
 874
 875       -- we should never see a equality
 876     go (PredTy (EqPred _ _))
 877       = panic "TcTyFuns.flattenType: malformed type"
 878
 879     go _ = panic "TcTyFuns: suppress bogus warning"
 880
 881 adjustCoercions :: EqInstCo            -- coercion of original equality
 882                 -> Coercion            -- coercion witnessing the left rewrite
 883                 -> Coercion            -- coercion witnessing the right rewrite
 884                 -> (Type, Type)        -- types of flattened equality
 885                 -> [RewriteInst]       -- equalities from flattening
 886                 -> TcM (EqInstCo,      -- coercion for flattened equality
 887                         [RewriteInst]) -- final equalities from flattening
 888 -- Depending on whether we flattened a local or wanted equality, that equality's
 889 -- coercion and that of the new equalities produced during flattening are
 890 -- adjusted .
 891 adjustCoercions (Left cotv) co1 co2 (ty_l, ty_r) all_eqs
 892     -- wanted => generate a fresh coercion variable for the flattened equality
 893   = do { cotv' <- newMetaCoVar ty_l ty_r
 894        ; bindMetaTyVar cotv $
 895            (co1 `mkTransCoercion` TyVarTy cotv' `mkTransCoercion` co2)
 896        ; return (Left cotv', all_eqs)
 897        }
 898
 899 adjustCoercions co@(Right _) _co1 _co2 _eqTys all_eqs
 900     -- local => turn all new equalities into locals and update (but not zonk)
 901     --          the skolem
 902   = do { all_eqs' <- mapM wantedToLocal all_eqs
 903        ; return (co, all_eqs')
 904        }
 905
 906 mkDictBind :: Inst                 -- original instance
 907            -> Bool                 -- is this a wanted contraint?
 908            -> Coercion             -- coercion witnessing the rewrite
 909            -> PredType             -- coerced predicate
 910            -> TcM (Inst,           -- new inst
 911                    TcDictBinds)    -- binding for coerced dictionary
 912 mkDictBind dict isWanted rewriteCo pred
 913   = do { dict' <- newDictBndr loc pred
 914          -- relate the old inst to the new one
 915          -- target_dict = source_dict `cast` st_co
 916        ; let (target_dict, source_dict, st_co)
 917                | isWanted  = (dict,  dict', mkSymCoercion rewriteCo)
 918                | otherwise = (dict', dict,  rewriteCo)
 919                  -- we have
 920                  --   co :: dict ~ dict'
 921                  -- hence, if isWanted
 922                  --       dict  = dict' `cast` sym co
 923                  --        else
 924                  --       dict' = dict  `cast` co
 925              expr      = HsVar $ instToId source_dict
 926              cast_expr = HsWrap (WpCast st_co) expr
 927              rhs       = L (instLocSpan loc) cast_expr
 928              binds     = instToDictBind target_dict rhs
 929        ; return (dict', binds)
 930        }
 931   where
 932     loc = tci_loc dict
 933
 934 -- gamma ::^l Fam args ~ alpha
 935 -- => gamma ::^w Fam args ~ alpha, with alpha := Fam args & gamma := Fam args
 936 --    (the update of alpha will not be apparent during propagation, as we
 937 --    never follow the indirections of meta variables; it will be revealed
 938 --    when the equality is zonked)
 939 --
 940 --  NB: It's crucial to update *both* alpha and gamma, as gamma may already
 941 --      have escaped into some other coercions during normalisation.
 942 --
 943 --      We do actually update alpha and gamma by side effect (instead of
 944 --      only remembering the binding with `bindMetaTyVar', as we do for all
 945 --      other tyvars).  We can do this as the side effects are strictly
 946 --      *local*; we know that both alpha and gamma were just a moment ago
 947 --      introduced by normalisation.
 948 --
 949 wantedToLocal :: RewriteInst -> TcM RewriteInst
 950 wantedToLocal eq@(RewriteFam {rwi_fam   = fam,
 951                               rwi_args  = args,
 952                               rwi_right = TyVarTy alpha,
 953                               rwi_co    = Left gamma})
 954   = do { writeMetaTyVar alpha (mkTyConApp fam args)
 955        ; writeMetaTyVar gamma (mkTyConApp fam args)
 956        ; return $ eq {rwi_co = mkGivenCo $ mkTyVarTy gamma}
 957        }
 958 wantedToLocal _ = panic "TcTyFuns.wantedToLocal"
 959 \end{code}
 960
 961
 962 %************************************************************************
 963 %*                                                                      *
 964                 Propagation of equalities
 965 %*                                                                      *
 966 %************************************************************************
 967
 968 Apply the propagation rules exhaustively.
 969
 970 \begin{code}
 971 propagate :: [RewriteInst] -> EqConfig -> TcM EqConfig
 972 propagate []       eqCfg = return eqCfg
 973 propagate (eq:eqs) eqCfg
 974   = do { optEqs <- applyTop eq
 975        ; case optEqs of
 976
 977               -- Top applied to 'eq' => retry with new equalities
 978            Just eqs2 -> propagate (eqs2 ++ eqs) eqCfg
 979
 980               -- Top doesn't apply => try subst rules with all other
 981               --   equalities, after that 'eq' can go into the residual list
 982            Nothing   -> do { (eqs', eqCfg') <- applySubstRules eq eqs eqCfg
 983                            ; propagate eqs' (eqCfg' `addEq` eq)
 984                            }
 985        }
 986
 987 applySubstRules :: RewriteInst                    -- currently considered eq
 988                 -> [RewriteInst]                  -- todo eqs list
 989                 -> EqConfig                       -- residual
 990                 -> TcM ([RewriteInst], EqConfig)  -- new todo & residual
 991 applySubstRules eq todoEqs (eqConfig@EqConfig {eqs = resEqs})
 992   = do { (newEqs_t, unchangedEqs_t) <- mapSubstRules eq todoEqs
 993        ; (newEqs_r, unchangedEqs_r) <- mapSubstRules eq resEqs
 994        ; return (newEqs_t ++ newEqs_r ++ unchangedEqs_t,
 995                  eqConfig {eqs = unchangedEqs_r})
 996        }
 997
 998 mapSubstRules :: RewriteInst     -- try substituting this equality
 999               -> [RewriteInst]   -- into these equalities
1000               -> TcM ([RewriteInst], [RewriteInst])
1001 mapSubstRules eq eqs
1002   = do { (newEqss, unchangedEqss) <- mapAndUnzipM (substRules eq) eqs
1003        ; return (concat newEqss, concat unchangedEqss)
1004        }
1005   where
1006     substRules eq1 eq2
1007       = do {traceTc $ hang (ptext (sLit "Trying subst rules with"))
1008                         4 (ppr eq1 $$ ppr eq2)
1009
1010                -- try the SubstFam rule
1011            ; optEqs <- applySubstFam eq1 eq2
1012            ; case optEqs of
1013                Just eqs -> return (eqs, [])
1014                Nothing  -> do
1015            {   -- try the SubstVarVar rule
1016              optEqs <- applySubstVarVar eq1 eq2
1017            ; case optEqs of
1018                Just eqs -> return (eqs, [])
1019                Nothing  -> do
1020            {   -- try the SubstVarFam rule
1021              optEqs <- applySubstVarFam eq1 eq2
1022            ; case optEqs of
1023                Just eq -> return ([eq], [])
1024                Nothing -> return ([], [eq2])
1025                  -- if no rule matches, we return the equlity we tried to
1026                  -- substitute into unchanged
1027            }}}
1028 \end{code}
1029
1030 Attempt to apply the Top rule.  The rule is
1031
1032   co :: F t1..tn ~ t
1033   =(Top)=>
1034   co' :: [s1/x1, .., sm/xm]s ~ t with co = g s1..sm |> co'
1035
1036 where g :: forall x1..xm. F u1..um ~ s and [s1/x1, .., sm/xm]u1 == t1.
1037
1038 Returns Nothing if the rule could not be applied.  Otherwise, the resulting
1039 equality is normalised and a list of the normal equalities is returned.
1040
1041 \begin{code}
1042 applyTop :: RewriteInst -> TcM (Maybe [RewriteInst])
1043
1044 applyTop eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
1045   = do { optTyCo <- tcUnfoldSynFamInst (TyConApp fam args)
1046        ; case optTyCo of
1047            Nothing                -> return Nothing
1048            Just (lhs, rewrite_co)
1049              -> do { co' <- mkRightTransEqInstCo co rewrite_co (lhs, rhs)
1050                    ; eq' <- deriveEqInst eq lhs rhs co'
1051                    ; liftM Just $ normEqInst eq'
1052                    }
1053        }
1054   where
1055     co  = rwi_co eq
1056     rhs = rwi_right eq
1057
1058 applyTop _ = return Nothing
1059 \end{code}
1060
1061 Attempt to apply the SubstFam rule.  The rule is
1062
1063   co1 :: F t1..tn ~ t  &  co2 :: F t1..tn ~ s
1064   =(SubstFam)=>
1065   co1 :: F t1..tn ~ t  &  co2' :: t ~ s with co2 = co1 |> co2'
1066
1067 where co1 may be a wanted only if co2 is a wanted, too.
1068
1069 Returns Nothing if the rule could not be applied.  Otherwise, the equality
1070 co2' is normalised and a list of the normal equalities is returned.  (The
1071 equality co1 is not returned as it remain unaltered.)
1072
1073 \begin{code}
1074 applySubstFam :: RewriteInst
1075               -> RewriteInst
1076               -> TcM (Maybe ([RewriteInst]))
1077 applySubstFam eq1@(RewriteFam {rwi_fam = fam1, rwi_args = args1})
1078               eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
1079
1080     -- rule matches => rewrite
1081   | fam1 == fam2 && tcEqTypes args1 args2 &&
1082     (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
1083   = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
1084        ; eq2' <- deriveEqInst eq2 lhs rhs co2'
1085        ; liftM Just $ normEqInst eq2'
1086        }
1087
1088     -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
1089   | fam1 == fam2 && tcEqTypes args1 args2 &&
1090     (isWantedRewriteInst eq1 || not (isWantedRewriteInst eq2))
1091   = return $ Just [eq2]
1092
1093   where
1094     lhs = rwi_right eq1
1095     rhs = rwi_right eq2
1096     co1 = eqInstCoType (rwi_co eq1)
1097     co2 = rwi_co eq2
1098
1099 applySubstFam _ _ = return Nothing
1100 \end{code}
1101
1102 Attempt to apply the SubstVarVar rule.  The rule is
1103
1104   co1 :: x ~ t  &  co2 :: x ~ s
1105   =(SubstVarVar)=>
1106   co1 :: x ~ t  &  co2' :: t ~ s with co2 = co1 |> co2'
1107
1108 where co1 may be a wanted only if co2 is a wanted, too.
1109
1110 Returns Nothing if the rule could not be applied.  Otherwise, the equality
1111 co2' is normalised and a list of the normal equalities is returned.  (The
1112 equality co1 is not returned as it remain unaltered.)
1113
1114 \begin{code}
1115 applySubstVarVar :: RewriteInst -> RewriteInst -> TcM (Maybe [RewriteInst])
1116 applySubstVarVar eq1@(RewriteVar {rwi_var = tv1})
1117                  eq2@(RewriteVar {rwi_var = tv2})
1118
1119     -- rule matches => rewrite
1120   | tv1 == tv2 &&
1121     (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
1122   = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
1123        ; eq2' <- deriveEqInst eq2 lhs rhs co2'
1124        ; liftM Just $ normEqInst eq2'
1125        }
1126
1127     -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
1128   | tv1 == tv2 &&
1129     (isWantedRewriteInst eq1 || not (isWantedRewriteInst eq2))
1130   = return $ Just [eq2]
1131
1132   where
1133     lhs = rwi_right eq1
1134     rhs = rwi_right eq2
1135     co1 = eqInstCoType (rwi_co eq1)
1136     co2 = rwi_co eq2
1137
1138 applySubstVarVar _ _ = return Nothing
1139 \end{code}
1140
1141 Attempt to apply the SubstVarFam rule.  The rule is
1142
1143   co1 :: x ~ t  &  co2 :: F s1..sn ~ s
1144   =(SubstVarFam)=>
1145   co1 :: x ~ t  &  co2' :: [t/x](F s1..sn) ~ s
1146     with co2 = [co1/x](F s1..sn) |> co2'
1147
1148 where x occurs in F s1..sn. (co1 may be local or wanted.)
1149
1150 Returns Nothing if the rule could not be applied.  Otherwise, the equality
1151 co2' is returned.  (The equality co1 is not returned as it remain unaltered.)
1152
1153 \begin{code}
1154 applySubstVarFam :: RewriteInst -> RewriteInst -> TcM (Maybe RewriteInst)
1155
1156   -- rule matches => rewrite
1157 applySubstVarFam eq1@(RewriteVar {rwi_var = tv1})
1158                  eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
1159   | tv1 `elemVarSet` tyVarsOfTypes args2
1160   = do { let co1Subst = substTyWith [tv1] [co1] (mkTyConApp fam2 args2)
1161              args2'   = substTysWith [tv1] [rhs1] args2
1162              lhs2     = mkTyConApp fam2 args2'
1163        ; co2' <- mkRightTransEqInstCo co2 co1Subst (lhs2, rhs2)
1164        ; return $ Just (eq2 {rwi_args = args2', rwi_co = co2'})
1165        }
1166   where
1167     rhs1 = rwi_right eq1
1168     rhs2 = rwi_right eq2
1169     co1  = eqInstCoType (rwi_co eq1)
1170     co2  = rwi_co eq2
1171
1172   -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
1173 applySubstVarFam (RewriteFam {rwi_args = args1})
1174                  eq2@(RewriteVar {rwi_var = tv2})
1175   | tv2 `elemVarSet` tyVarsOfTypes args1
1176   = return $ Just eq2
1177
1178 applySubstVarFam _ _ = return Nothing
1179 \end{code}
1180
1181
1182 %************************************************************************
1183 %*                                                                      *
1184                 Finalisation of equalities
1185 %*                                                                      *
1186 %************************************************************************
1187
1188 Exhaustive substitution of all variable equalities of the form co :: x ~ t
1189 (both local and wanted) into the right-hand sides of all other equalities and
1190 of family equalities of the form co :: F t1..tn ~ alpha into both sides of all
1191 other *family* equalities.  This may lead to recursive equalities; i.e., (1)
1192 we need to apply the substitution implied by one equality exhaustively before
1193 turning to the next and (2) we need an occurs check.
1194
1195 We also apply the same substitutions to the local and wanted class and IP
1196 dictionaries.
1197
1198 We perform the substitutions in two steps:
1199
1200   Step A: Substitute variable equalities into the right-hand sides of all
1201           other equalities (but wanted only into wanteds) and into class and IP
1202           constraints (again wanteds only into wanteds).
1203
1204   Step B: Substitute wanted family equalities `co :: F t1..tn ~ alpha', where
1205           'alpha' is a skolem flexible (i.e., not free in the environment),
1206           into the right-hand sides of all wanted variable equalities and into
1207           both sides of all wanted family equalities.
1208
1209   Step C: Substitute the remaining wanted family equalities `co :: F t1..tn ~
1210           alpha' into the right-hand sides of all wanted variable equalities
1211           and into both sides of all wanted family equalities.
1212
1213 In inference mode, we do not substitute into variable equalities in Steps B & C.
1214
1215 The treatment of flexibles in wanteds is quite subtle.  We absolutely want to
1216 substitute variable equalities first; e.g., consider
1217
1218   F s ~ alpha, alpha ~ t
1219
1220 If we don't substitute `alpha ~ t', we may instantiate `t' with `F s' instead.
1221 This would be bad as `F s' is less useful, eg, as an argument to a class
1222 constraint.
1223
1224 The restriction on substituting locals is necessary due to examples, such as
1225
1226   F delta ~ alpha, F alpha ~ delta,
1227
1228 where `alpha' is a skolem flexible and `delta' a environment flexible. We need
1229 to produce `F (F delta) ~ delta' (and not `F (F alpha) ~ alpha'). Otherwise,
1230 we may wrongly claim to having performed an improvement, which can lead to
1231 non-termination of the combined class-family solver.
1232
1233 We do also substitute flexibles, as in `alpha ~ t' into class constraints.
1234 When `alpha' is later instantiated, we'd get the same effect, but in the
1235 meantime the class constraint would miss some information, which would be a
1236 problem in an integrated equality-class solver.
1237
1238 NB:
1239 * Given that we apply the substitution corresponding to a single equality
1240   exhaustively, before turning to the next, and because we eliminate recursive
1241   equalities, all opportunities for subtitution will have been exhausted after
1242   we have considered each equality once.
1243
1244 \begin{code}
1245 substitute :: [RewriteInst]       -- equalities
1246            -> [Inst]              -- local class dictionaries
1247            -> [Inst]              -- wanted class dictionaries
1248            -> Bool                -- True ~ checking mode; False ~ inference
1249            -> TyVarSet            -- flexibles free in the environment
1250            -> TcM ([RewriteInst], -- equalities after substitution
1251                    TcDictBinds,   -- all newly generated dictionary bindings
1252                    [Inst],        -- local dictionaries after substitution
1253                    [Inst])        -- wanted dictionaries after substitution
1254 substitute eqs locals wanteds checkingMode freeFlexibles
1255   = -- We achieve the sequencing of "Step A", "Step B", and "Step C" above by
1256     -- sorting the equalities appropriately: first all variable, then all
1257     -- family/skolem, and then the remaining family equalities.
1258     let (var_eqs, fam_eqs)             = partition isRewriteVar eqs
1259         (fam_skolem_eqs, fam_eqs_rest) = partition isFamSkolemEq fam_eqs
1260     in
1261     subst (var_eqs ++ fam_skolem_eqs ++ fam_eqs_rest) [] emptyBag locals wanteds
1262   where
1263     isFamSkolemEq (RewriteFam {rwi_right = ty})
1264       | Just tv <- tcGetTyVar_maybe ty = not (tv `elemVarSet` freeFlexibles)
1265     isFamSkolemEq _ = False
1266
1267     subst [] res binds locals wanteds
1268       = return (res, binds, locals, wanteds)
1269
1270     -- co :: x ~ t
1271     subst (eq@(RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}):eqs)
1272           res binds locals wanteds
1273       = do { traceTc $ ptext (sLit "TcTyFuns.substitute[RewriteVar]:") <+>
1274                        ppr eq
1275
1276              -- create the substitution
1277            ; let coSubst = zipOpenTvSubst [tv] [eqInstCoType co]
1278                  tySubst = zipOpenTvSubst [tv] [ty]
1279
1280              -- substitute into all other equalities
1281            ; eqs' <- mapM (substEq eq coSubst tySubst) eqs
1282            ; res' <- mapM (substEq eq coSubst tySubst) res
1283
1284              -- only substitute local equalities into local dictionaries
1285            ; (lbinds, locals')  <- if not (isWantedCo co)
1286                                    then
1287                                      mapAndUnzipM
1288                                        (substDict eq coSubst tySubst False)
1289                                        locals
1290                                    else
1291                                      return ([], locals)
1292
1293               -- substitute all equalities into wanteds dictionaries
1294            ; (wbinds, wanteds') <- mapAndUnzipM
1295                                      (substDict eq coSubst tySubst True)
1296                                      wanteds
1297
1298            ; let binds' = unionManyBags $ binds : lbinds ++ wbinds
1299            ; subst eqs' (eq:res') binds' locals' wanteds'
1300            }
1301
1302     -- co ::^w F t1..tn ~ alpha
1303     subst (eq@(RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = ty,
1304                            rwi_co = co}):eqs)
1305           res binds locals wanteds
1306       | Just tv <- tcGetTyVar_maybe ty
1307       , isMetaTyVar tv
1308       , isWantedCo co
1309       = do { traceTc $ ptext (sLit "TcTyFuns.substitute[RewriteFam]:") <+>
1310                        ppr eq
1311
1312              -- create the substitution
1313            ; let coSubst = zipOpenTvSubst [tv] [mkSymCoercion $ eqInstCoType co]
1314                  tySubst = zipOpenTvSubst [tv] [mkTyConApp fam args]
1315
1316              -- substitute into other wanted equalities (`substEq' makes sure
1317              -- that we only substitute into wanteds)
1318            ; eqs' <- mapM (substEq eq coSubst tySubst) eqs
1319            ; res' <- mapM (substEq eq coSubst tySubst) res
1320
1321            ; subst eqs' (eq:res') binds locals wanteds
1322            }
1323
1324     subst (eq:eqs) res binds locals wanteds
1325       = subst eqs (eq:res) binds locals wanteds
1326
1327       -- We have, co :: tv ~ ty
1328       -- => apply [ty/tv] to right-hand side of eq2
1329       --    (but only if tv actually occurs in the right-hand side of eq2
1330       --    and if eq2 is a local, co :: tv ~ ty needs to be a local, too)
1331     substEq (RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co})
1332             coSubst tySubst eq2
1333       |  tv `elemVarSet` tyVarsOfType (rwi_right eq2)
1334       && (isWantedRewriteInst eq2 || not (isWantedCo co))
1335       = do { let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
1336                  right2'  = substTy tySubst (rwi_right eq2)
1337                  left2    = case eq2 of
1338                               RewriteVar {rwi_var = tv2}   -> mkTyVarTy tv2
1339                               RewriteFam {rwi_fam = fam,
1340                                           rwi_args = args} ->mkTyConApp fam args
1341            ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2')
1342            ; case eq2 of
1343                RewriteVar {rwi_var = tv2} | tv2 `elemVarSet` tyVarsOfType ty
1344                  -> occurCheckErr left2 right2'
1345                _ -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
1346            }
1347
1348       -- We have, co ::^w F t1..tn ~ tv
1349       -- => apply [F t1..tn/tv] to eq2
1350       --    (but only if tv actually occurs in eq2
1351       --    and eq2 is a wanted equality
1352       --    and we are either in checking mode or eq2 is a family equality)
1353     substEq (RewriteFam {rwi_args = args, rwi_right = ty})
1354             coSubst tySubst eq2
1355       | Just tv <- tcGetTyVar_maybe ty
1356       , tv `elemVarSet` tyVarsOfRewriteInst eq2
1357       , isWantedRewriteInst eq2
1358       , checkingMode || not (isRewriteVar eq2)
1359       = do { -- substitute into the right-hand side
1360            ; let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
1361                  right2'  = substTy tySubst (rwi_right eq2)
1362                  left2    = case eq2 of
1363                               RewriteVar {rwi_var = tv2}   -> mkTyVarTy tv2
1364                               RewriteFam {rwi_fam = fam,
1365                                           rwi_args = args} -> mkTyConApp fam args
1366            ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2')
1367            ; case eq2 of
1368                RewriteVar {rwi_var = tv2}
1369                  -- variable equality: perform an occurs check
1370                  | tv2 `elemVarSet` tyVarsOfTypes args
1371                  -> occurCheckErr left2 right2'
1372                  | otherwise
1373                  -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
1374                RewriteFam {rwi_fam = fam}
1375                  -- family equality: substitute also into the left-hand side
1376                  -> do { let co1Subst = substTy coSubst left2
1377                              args2'   = substTys tySubst (rwi_args  eq2)
1378                              left2'   = mkTyConApp fam args2'
1379                        ; co2'' <- mkRightTransEqInstCo co2' co1Subst
1380                                                        (left2', right2')
1381                        ; return $ eq2 {rwi_args = args2', rwi_right = right2',
1382                                        rwi_co = co2''}
1383                        }
1384            }
1385
1386       -- unchanged
1387     substEq _ _ _ eq2
1388       = return eq2
1389
1390       -- We have, co :: tv ~ ty
1391       -- => apply [ty/tv] to dictionary predicate
1392       --    (but only if tv actually occurs in the predicate)
1393     substDict (RewriteVar {rwi_var = tv}) coSubst tySubst isWanted dict
1394       | isClassDict dict
1395       , tv `elemVarSet` tyVarsOfPred (tci_pred dict)
1396       = do { let co1Subst = PredTy (substPred coSubst (tci_pred dict))
1397                  pred'    = substPred tySubst (tci_pred dict)
1398            ; (dict', binds) <- mkDictBind dict isWanted co1Subst pred'
1399            ; return (binds, dict')
1400            }
1401
1402       -- unchanged
1403     substDict _ _ _ _ dict
1404       = return (emptyBag, dict)
1405 -- !!!TODO: Still need to substitute into IP constraints.
1406 \end{code}
1407
1408 For any *wanted* variable equality of the form co :: alpha ~ t or co :: a ~
1409 alpha, we record a binding of alpha with t or a, respectively, and for co :=
1410 id.  We do the same for equalities of the form co :: F t1..tn ~ alpha unless
1411 we are in inference mode and alpha appears in the environment - i.e., it is
1412 not a flexible introduced by flattening locals or it is local, but was
1413 propagated into the environment by the instantiation of a variable equality.
1414
1415 We proceed in two phases: (1) first we consider all variable equalities and then
1416 (2) we consider all family equalities.  The two phase structure is required as
1417 the recorded variable equalities determine which skolems flexibles escape, and
1418 hence, which family equalities may be recorded as bindings.
1419
1420 We return all wanted equalities for which we did not generate a binding.
1421 (These can be skolem variable equalities, cyclic variable equalities, and
1422 family equalities.)
1423
1424 We don't update any meta variables.  Instead, instantiation simply implies
1425 putting a type variable binding into the binding pool of TcM.
1426
1427 NB:
1428  * We may encounter filled flexibles due to the instant filling of local
1429    skolems in local-given constraints during flattening.
1430  * Be careful with SigTVs.  They can only be instantiated with other SigTVs or
1431    rigid skolems.
1432
1433 \begin{code}
1434 bindAndExtract :: [RewriteInst] -> Bool -> TyVarSet -> TcM [Inst]
1435 bindAndExtract eqs checkingMode freeFlexibles
1436   = do { traceTc $ hang (ptext (sLit "bindAndExtract:"))
1437                      4 (ppr eqs $$ ppr freeFlexibles)
1438        ; residuals1 <- mapMaybeM instVarEq (filter isWantedRewriteInst eqs)
1439        ; escapingSkolems <- getEscapingSkolems
1440        ; let newFreeFlexibles = freeFlexibles `unionVarSet` escapingSkolems
1441        ; residuals2 <- mapMaybeM (instFamEq newFreeFlexibles) residuals1
1442        ; mapM rewriteInstToInst residuals2
1443        }
1444   where
1445     -- NB: we don't have to transitively chase the relation as the substitution
1446     --     process applied before generating the bindings was exhaustive
1447     getEscapingSkolems
1448       = do { tybinds_rel <- getTcTyVarBindsRelation
1449            ; return (unionVarSets . map snd . filter isFree $ tybinds_rel)
1450            }
1451       where
1452         isFree (tv, _) = tv `elemVarSet` freeFlexibles
1453
1454         -- co :: alpha ~ t or co :: a ~ alpha
1455     instVarEq eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co})
1456       = do { flexi_tv1       <- isFlexible   tv1
1457            ; maybe_flexi_tv2 <- isFlexibleTy ty2
1458            ; case (flexi_tv1, maybe_flexi_tv2) of
1459                (True, Just tv2)
1460                  | isSigTyVar tv1 && isSigTyVar tv2
1461                  -> -- co :: alpha ~ beta, where both a SigTvs
1462                     doInst (rwi_swapped eq) tv1 ty2 co eq
1463                (True, Nothing)
1464                  | Just tv2 <- tcGetTyVar_maybe ty2
1465                  , isSigTyVar tv1
1466                  , isSkolemTyVar tv2
1467                  -> -- co :: alpha ~ a, where alpha is a SigTv
1468                     doInst (rwi_swapped eq) tv1 ty2 co eq
1469                (True, _)
1470                  | not (isSigTyVar tv1)
1471                  -> -- co :: alpha ~ t, where alpha is not a SigTv
1472                     doInst (rwi_swapped eq) tv1 ty2 co eq
1473                (False, Just tv2)
1474                  | isSigTyVar tv2
1475                  , isSkolemTyVar tv1
1476                  -> -- co :: a ~ alpha, where alpha is a SigTv
1477                     doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
1478                  | not (isSigTyVar tv2)
1479                  -> -- co :: a ~ alpha, where alpha is not a SigTv
1480                     --                        ('a' may be filled)
1481                     doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
1482                _ -> return $ Just eq
1483            }
1484     instVarEq eq = return $ Just eq
1485
1486         -- co :: F args ~ alpha,
1487         -- and we are either in checking mode or alpha is a skolem flexible that
1488         --     doesn't escape
1489     instFamEq newFreeFlexibles eq@(RewriteFam {rwi_fam = fam, rwi_args = args,
1490                                                rwi_right = ty2, rwi_co = co})
1491       | Just tv2 <- tcGetTyVar_maybe ty2
1492       , checkingMode || not (tv2 `elemVarSet` newFreeFlexibles)
1493       = do { flexi_tv2 <- isFlexible tv2
1494            ; if flexi_tv2
1495              then
1496                doInst (not $ rwi_swapped eq) tv2 (mkTyConApp fam args) co eq
1497              else
1498                return $ Just eq
1499            }
1500     instFamEq _ eq = return $ Just eq
1501
1502     -- tv is a meta var, but not a SigTV and not filled
1503     isFlexible tv
1504       | isMetaTyVar tv = liftM isFlexi $ readMetaTyVar tv
1505       | otherwise      = return False
1506
1507     -- type is a tv that is a meta var, but not a SigTV and not filled
1508     isFlexibleTy ty
1509       | Just tv <- tcGetTyVar_maybe ty = do {flexi <- isFlexible tv
1510                                             ; if flexi then return $ Just tv
1511                                                        else return Nothing
1512                                             }
1513       | otherwise                      = return Nothing
1514
1515     doInst _swapped _tv _ty (Right ty) _eq
1516       = pprPanic "TcTyFuns.doInst: local eq: " (ppr ty)
1517     doInst swapped tv ty (Left cotv) eq
1518       = do { lookupTV <- lookupTcTyVar tv
1519            ; bMeta swapped tv lookupTV ty cotv
1520            }
1521       where
1522         -- Try to create a binding for a meta variable.  There is *no* need to
1523         -- consider reorienting the underlying equality; `checkOrientation'
1524         -- makes sure that we get variable-variable equalities only in the
1525         -- appropriate orientation.
1526         --
1527         bMeta :: Bool                    -- is this a swapped equality?
1528               -> TcTyVar                 -- tyvar to instantiate
1529               -> LookupTyVarResult       -- lookup result of that tyvar
1530               -> TcType                  -- to to instantiate tyvar with
1531               -> TcTyVar                 -- coercion tyvar of current equality
1532               -> TcM (Maybe RewriteInst) -- returns the original equality if
1533                                          -- the tyvar could not be instantiated,
1534                                          -- and hence, the equality must be kept
1535
1536         -- meta variable has been filled already
1537         -- => this should never happen due to the use of `isFlexible' above
1538         bMeta _swapped tv (IndirectTv fill_ty) ty _cotv
1539           = pprPanic "TcTyFuns.bMeta" $
1540               ptext (sLit "flexible") <+> ppr tv <+>
1541               ptext (sLit "already filled with") <+> ppr fill_ty <+>
1542               ptext (sLit "meant to fill with") <+> ppr ty
1543
1544         -- type variable meets type variable
1545         -- => `checkOrientation' already ensures that it is fine to instantiate
1546         --    tv1 with tv2, but chase tv2's instantiations if necessary, so that
1547         --    we eventually can perform a kinds check in bMetaInst
1548         -- NB: tv's instantiations won't alter the orientation in which we
1549         --     want to instantiate as they either constitute a family
1550         --     application or are themselves due to a properly oriented
1551         --     instantiation
1552         bMeta swapped tv1 details1@(DoneTv (MetaTv _ _)) ty@(TyVarTy tv2) cotv
1553           = do { lookupTV2 <- lookupTcTyVar tv2
1554                ; case lookupTV2 of
1555                    IndirectTv ty' -> bMeta swapped tv1 details1 ty' cotv
1556                    DoneTv _       -> bMetaInst swapped tv1 ty cotv
1557                }
1558
1559         -- updatable meta variable meets non-variable type
1560         -- => occurs check, monotype check, and kinds match check, then bind
1561         bMeta swapped tv (DoneTv (MetaTv _ _ref)) non_tv_ty cotv
1562           = bMetaInst swapped tv non_tv_ty cotv
1563
1564         bMeta _ _ _ _ _ = panic "TcTyFuns.bMeta"
1565
1566         -- We know `tv' can be instantiated; check that `ty' is alright for
1567         -- instantiating `tv' with and then record a binding; we return the
1568         -- original equality if it is cyclic through a synonym family
1569         bMetaInst swapped tv ty cotv
1570           = do {   -- occurs + monotype check
1571                ; mb_ty' <- checkTauTvUpdate tv ty
1572
1573                ; case mb_ty' of
1574                    Nothing  ->
1575                      -- there may be a family in non_tv_ty due to an unzonked,
1576                      -- but updated skolem for a local equality
1577                      -- (cf `wantedToLocal')
1578                      return $ Just eq
1579                    Just ty' ->
1580                      do { checkKinds swapped tv ty'
1581                         ; bindMetaTyVar tv ty'          -- bind meta var
1582                         ; bindMetaTyVar cotv ty'        -- bind co var
1583                         ; return Nothing
1584                         }
1585                }
1586 \end{code}
1587
1588
1589 %************************************************************************
1590 %*                                                                      *
1591 \section{Errors}
1592 %*                                                                      *
1593 %************************************************************************
1594
1595 The infamous couldn't match expected type soandso against inferred type
1596 somethingdifferent message.
1597
1598 \begin{code}
1599 eqInstMisMatch :: Inst -> TcM a
1600 eqInstMisMatch inst
1601   = ASSERT( isEqInst inst )
1602     setInstCtxt (instLoc inst) $ failWithMisMatch ty_act ty_exp
1603   where
1604     (ty_act, ty_exp) = eqInstTys inst
1605
1606 -----------------------
1607 failWithMisMatch :: TcType -> TcType -> TcM a
1608 -- Generate the message when two types fail to match,
1609 -- going to some trouble to make it helpful.
1610 -- The argument order is: actual type, expected type
1611 failWithMisMatch ty_act ty_exp
1612   = do  { env0 <- tcInitTidyEnv
1613         ; ty_exp <- zonkTcType ty_exp
1614         ; ty_act <- zonkTcType ty_act
1615         ; failWithTcM (misMatchMsg env0 (ty_act, ty_exp))
1616         }
1617
1618 misMatchMsg :: TidyEnv -> (TcType, TcType) -> (TidyEnv, SDoc)
1619 misMatchMsg env0 (ty_act, ty_exp)
1620   = let (env1, pp_exp, extra_exp) = ppr_ty env0 ty_exp
1621         (env2, pp_act, extra_act) = ppr_ty env1 ty_act
1622         msg = sep [sep [ptext (sLit "Couldn't match expected type") <+> pp_exp,
1623                         nest 7 $
1624                               ptext (sLit "against inferred type") <+> pp_act],
1625                    nest 2 (extra_exp $$ extra_act $$ extra_tyfun) ]
1626                         -- See Note [Non-injective type functions]
1627     in
1628     (env2, msg)
1629
1630   where
1631     extra_tyfun
1632       = case (tcSplitTyConApp_maybe ty_act, tcSplitTyConApp_maybe ty_exp) of
1633           (Just (tc_act,_), Just (tc_exp,_)) | tc_act == tc_exp
1634               -> if isOpenSynTyCon tc_act then pp_open_tc tc_act
1635                  else WARN( True, ppr tc_act) -- If there's a mis-match, then
1636                       empty                   -- it should be a family
1637           _ -> empty
1638
1639     pp_open_tc tc = ptext (sLit "NB:") <+> quotes (ppr tc)
1640                     <+> ptext (sLit "is a type function") <> pp_inj
1641         where
1642           pp_inj | isInjectiveTyCon tc = empty
1643                  | otherwise = ptext (sLit (", and may not be injective"))
1644
1645     ppr_ty :: TidyEnv -> TcType -> (TidyEnv, SDoc, SDoc)
1646     ppr_ty env ty
1647       = let (env1, tidy_ty) = tidyOpenType env ty
1648             (env2, extra)  = ppr_extra env1 tidy_ty
1649         in
1650         (env2, quotes (ppr tidy_ty), extra)
1651
1652     -- (ppr_extra env ty) shows extra info about 'ty'
1653     ppr_extra :: TidyEnv -> Type -> (TidyEnv, SDoc)
1654     ppr_extra env (TyVarTy tv)
1655       | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv) && not (isUnk tv)
1656       = (env1, pprSkolTvBinding tv1)
1657       where
1658         (env1, tv1) = tidySkolemTyVar env tv
1659
1660     ppr_extra env _ty = (env, empty)            -- Normal case
1661 \end{code}
1662
1663 Note [Non-injective type functions]
1664 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1665 It's very confusing to get a message like
1666      Couldn't match expected type `Depend s'
1667             against inferred type `Depend s1'
1668 so pp_open_tc adds:
1669        NB: `Depend' is type function, and hence may not be injective
1670
1671 Warn of loopy local equalities that were dropped.
1672
1673 \begin{code}
1674 warnDroppingLoopyEquality :: TcType -> TcType -> TcM ()
1675 warnDroppingLoopyEquality ty1 ty2
1676   = do { env0 <- tcInitTidyEnv
1677        ; ty1 <- zonkTcType ty1
1678        ; ty2 <- zonkTcType ty2
1679        ; let (env1 , tidy_ty1) = tidyOpenType env0 ty1
1680              (_env2, tidy_ty2) = tidyOpenType env1 ty2
1681        ; addWarnTc $ hang (ptext (sLit "Dropping loopy given equality"))
1682                        2 (quotes (ppr tidy_ty1 <+> text "~" <+> ppr tidy_ty2))
1683        }
1684 \end{code}