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 { ASSERTM2( allM 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       -- data 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            ; if null args_eqss
 803              then     -- unchanged, keep the old type with folded synonyms
 804                return (ty, ty, [])
 805              else
 806                return (mkTyConApp con args',
 807                        mkTyConApp con cargs,
 808                        concat args_eqss)
 809            }
 810
 811       -- function type => flatten subtypes
 812       -- NB: Special cased for efficiency - could be handled as type application
 813     go ty@(FunTy ty_l ty_r)
 814       = do { (ty_l', co_l, eqs_l) <- go ty_l
 815            ; (ty_r', co_r, eqs_r) <- go ty_r
 816            ; if null eqs_l && null eqs_r
 817              then     -- unchanged, keep the old type with folded synonyms
 818                return (ty, ty, [])
 819              else
 820                return (mkFunTy ty_l' ty_r',
 821                        mkFunTy co_l co_r,
 822                        eqs_l ++ eqs_r)
 823            }
 824
 825       -- type application => flatten subtypes
 826     go ty
 827       | Just (ty_l, ty_r) <- repSplitAppTy_maybe ty
 828                              -- need to use the smart split as ty may be an
 829                              -- oversaturated family application
 830       = do { (ty_l', co_l, eqs_l) <- go ty_l
 831            ; (ty_r', co_r, eqs_r) <- go ty_r
 832            ; if null eqs_l && null eqs_r
 833              then     -- unchanged, keep the old type with folded synonyms
 834                return (ty, ty, [])
 835              else
 836                return (mkAppTy ty_l' ty_r',
 837                        mkAppTy co_l co_r,
 838                        eqs_l ++ eqs_r)
 839            }
 840
 841       -- forall type => panic if the body contains a type family
 842       -- !!!TODO: As long as the family does not contain a quantified variable
 843       --          we might pull it out, but what if it does contain a quantified
 844       --          variable???
 845     go ty@(ForAllTy _ body)
 846       | null (tyFamInsts body)
 847       = return (ty, ty, [])
 848       | otherwise
 849       = panic "TcTyFuns.flattenType: synonym family in a rank-n type"
 850
 851       -- we should never see a predicate type
 852     go (PredTy _)
 853       = panic "TcTyFuns.flattenType: unexpected PredType"
 854
 855     go _ = panic "TcTyFuns: suppress bogus warning"
 856
 857 adjustCoercions :: EqInstCo            -- coercion of original equality
 858                 -> Coercion            -- coercion witnessing the left rewrite
 859                 -> Coercion            -- coercion witnessing the right rewrite
 860                 -> (Type, Type)        -- types of flattened equality
 861                 -> [RewriteInst]       -- equalities from flattening
 862                 -> TcM (EqInstCo,      -- coercion for flattened equality
 863                         [RewriteInst]) -- final equalities from flattening
 864 -- Depending on whether we flattened a local or wanted equality, that equality's
 865 -- coercion and that of the new equalities produced during flattening are
 866 -- adjusted .
 867 adjustCoercions (Left cotv) co1 co2 (ty_l, ty_r) all_eqs
 868     -- wanted => generate a fresh coercion variable for the flattened equality
 869   = do { cotv' <- newMetaCoVar ty_l ty_r
 870        ; bindMetaTyVar cotv $
 871            (co1 `mkTransCoercion` TyVarTy cotv' `mkTransCoercion` co2)
 872        ; return (Left cotv', all_eqs)
 873        }
 874
 875 adjustCoercions co@(Right _) _co1 _co2 _eqTys all_eqs
 876     -- local => turn all new equalities into locals and update (but not zonk)
 877     --          the skolem
 878   = do { all_eqs' <- mapM wantedToLocal all_eqs
 879        ; return (co, all_eqs')
 880        }
 881
 882 mkDictBind :: Inst                 -- original instance
 883            -> Bool                 -- is this a wanted contraint?
 884            -> Coercion             -- coercion witnessing the rewrite
 885            -> PredType             -- coerced predicate
 886            -> TcM (Inst,           -- new inst
 887                    TcDictBinds)    -- binding for coerced dictionary
 888 mkDictBind dict isWanted rewriteCo pred
 889   = do { dict' <- newDictBndr loc pred
 890          -- relate the old inst to the new one
 891          -- target_dict = source_dict `cast` st_co
 892        ; let (target_dict, source_dict, st_co)
 893                | isWanted  = (dict,  dict', mkSymCoercion rewriteCo)
 894                | otherwise = (dict', dict,  rewriteCo)
 895                  -- we have
 896                  --   co :: dict ~ dict'
 897                  -- hence, if isWanted
 898                  --       dict  = dict' `cast` sym co
 899                  --        else
 900                  --       dict' = dict  `cast` co
 901              expr      = HsVar $ instToId source_dict
 902              cast_expr = HsWrap (WpCast st_co) expr
 903              rhs       = L (instLocSpan loc) cast_expr
 904              binds     = instToDictBind target_dict rhs
 905        ; return (dict', binds)
 906        }
 907   where
 908     loc = tci_loc dict
 909
 910 -- gamma ::^l Fam args ~ alpha
 911 -- => gamma ::^w Fam args ~ alpha, with alpha := Fam args & gamma := Fam args
 912 --    (the update of alpha will not be apparent during propagation, as we
 913 --    never follow the indirections of meta variables; it will be revealed
 914 --    when the equality is zonked)
 915 --
 916 --  NB: It's crucial to update *both* alpha and gamma, as gamma may already
 917 --      have escaped into some other coercions during normalisation.
 918 --
 919 --      We do actually update alpha and gamma by side effect (instead of
 920 --      only remembering the binding with `bindMetaTyVar', as we do for all
 921 --      other tyvars).  We can do this as the side effects are strictly
 922 --      *local*; we know that both alpha and gamma were just a moment ago
 923 --      introduced by normalisation.
 924 --
 925 wantedToLocal :: RewriteInst -> TcM RewriteInst
 926 wantedToLocal eq@(RewriteFam {rwi_fam   = fam,
 927                               rwi_args  = args,
 928                               rwi_right = TyVarTy alpha,
 929                               rwi_co    = Left gamma})
 930   = do { writeMetaTyVar alpha (mkTyConApp fam args)
 931        ; writeMetaTyVar gamma (mkTyConApp fam args)
 932        ; return $ eq {rwi_co = mkGivenCo $ mkTyVarTy gamma}
 933        }
 934 wantedToLocal _ = panic "TcTyFuns.wantedToLocal"
 935 \end{code}
 936
 937
 938 %************************************************************************
 939 %*                                                                      *
 940                 Propagation of equalities
 941 %*                                                                      *
 942 %************************************************************************
 943
 944 Apply the propagation rules exhaustively.
 945
 946 \begin{code}
 947 propagate :: [RewriteInst] -> EqConfig -> TcM EqConfig
 948 propagate []       eqCfg = return eqCfg
 949 propagate (eq:eqs) eqCfg
 950   = do { optEqs <- applyTop eq
 951        ; case optEqs of
 952
 953               -- Top applied to 'eq' => retry with new equalities
 954            Just eqs2 -> propagate (eqs2 ++ eqs) eqCfg
 955
 956               -- Top doesn't apply => try subst rules with all other
 957               --   equalities, after that 'eq' can go into the residual list
 958            Nothing   -> do { (eqs', eqCfg') <- applySubstRules eq eqs eqCfg
 959                            ; propagate eqs' (eqCfg' `addEq` eq)
 960                            }
 961        }
 962
 963 applySubstRules :: RewriteInst                    -- currently considered eq
 964                 -> [RewriteInst]                  -- todo eqs list
 965                 -> EqConfig                       -- residual
 966                 -> TcM ([RewriteInst], EqConfig)  -- new todo & residual
 967 applySubstRules eq todoEqs (eqConfig@EqConfig {eqs = resEqs})
 968   = do { (newEqs_t, unchangedEqs_t) <- mapSubstRules eq todoEqs
 969        ; (newEqs_r, unchangedEqs_r) <- mapSubstRules eq resEqs
 970        ; return (newEqs_t ++ newEqs_r ++ unchangedEqs_t,
 971                  eqConfig {eqs = unchangedEqs_r})
 972        }
 973
 974 mapSubstRules :: RewriteInst     -- try substituting this equality
 975               -> [RewriteInst]   -- into these equalities
 976               -> TcM ([RewriteInst], [RewriteInst])
 977 mapSubstRules eq eqs
 978   = do { (newEqss, unchangedEqss) <- mapAndUnzipM (substRules eq) eqs
 979        ; return (concat newEqss, concat unchangedEqss)
 980        }
 981   where
 982     substRules eq1 eq2
 983       = do {traceTc $ hang (ptext (sLit "Trying subst rules with"))
 984                         4 (ppr eq1 $$ ppr eq2)
 985
 986                -- try the SubstFam rule
 987            ; optEqs <- applySubstFam eq1 eq2
 988            ; case optEqs of
 989                Just eqs -> return (eqs, [])
 990                Nothing  -> do
 991            {   -- try the SubstVarVar rule
 992              optEqs <- applySubstVarVar eq1 eq2
 993            ; case optEqs of
 994                Just eqs -> return (eqs, [])
 995                Nothing  -> do
 996            {   -- try the SubstVarFam rule
 997              optEqs <- applySubstVarFam eq1 eq2
 998            ; case optEqs of
 999                Just eq -> return ([eq], [])
1000                Nothing -> return ([], [eq2])
1001                  -- if no rule matches, we return the equlity we tried to
1002                  -- substitute into unchanged
1003            }}}
1004 \end{code}
1005
1006 Attempt to apply the Top rule.  The rule is
1007
1008   co :: F t1..tn ~ t
1009   =(Top)=>
1010   co' :: [s1/x1, .., sm/xm]s ~ t with co = g s1..sm |> co'
1011
1012 where g :: forall x1..xm. F u1..um ~ s and [s1/x1, .., sm/xm]u1 == t1.
1013
1014 Returns Nothing if the rule could not be applied.  Otherwise, the resulting
1015 equality is normalised and a list of the normal equalities is returned.
1016
1017 \begin{code}
1018 applyTop :: RewriteInst -> TcM (Maybe [RewriteInst])
1019
1020 applyTop eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
1021   = do { optTyCo <- tcUnfoldSynFamInst (TyConApp fam args)
1022        ; case optTyCo of
1023            Nothing                -> return Nothing
1024            Just (lhs, rewrite_co)
1025              -> do { co' <- mkRightTransEqInstCo co rewrite_co (lhs, rhs)
1026                    ; eq' <- deriveEqInst eq lhs rhs co'
1027                    ; liftM Just $ normEqInst eq'
1028                    }
1029        }
1030   where
1031     co  = rwi_co eq
1032     rhs = rwi_right eq
1033
1034 applyTop _ = return Nothing
1035 \end{code}
1036
1037 Attempt to apply the SubstFam rule.  The rule is
1038
1039   co1 :: F t1..tn ~ t  &  co2 :: F t1..tn ~ s
1040   =(SubstFam)=>
1041   co1 :: F t1..tn ~ t  &  co2' :: t ~ s with co2 = co1 |> co2'
1042
1043 where co1 may be a wanted only if co2 is a wanted, too.
1044
1045 Returns Nothing if the rule could not be applied.  Otherwise, the equality
1046 co2' is normalised and a list of the normal equalities is returned.  (The
1047 equality co1 is not returned as it remain unaltered.)
1048
1049 \begin{code}
1050 applySubstFam :: RewriteInst
1051               -> RewriteInst
1052               -> TcM (Maybe ([RewriteInst]))
1053 applySubstFam eq1@(RewriteFam {rwi_fam = fam1, rwi_args = args1})
1054               eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
1055
1056     -- rule matches => rewrite
1057   | fam1 == fam2 && tcEqTypes args1 args2 &&
1058     (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
1059   = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
1060        ; eq2' <- deriveEqInst eq2 lhs rhs co2'
1061        ; liftM Just $ normEqInst eq2'
1062        }
1063
1064     -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
1065   | fam1 == fam2 && tcEqTypes args1 args2 &&
1066     (isWantedRewriteInst eq1 || not (isWantedRewriteInst eq2))
1067   = return $ Just [eq2]
1068
1069   where
1070     lhs = rwi_right eq1
1071     rhs = rwi_right eq2
1072     co1 = eqInstCoType (rwi_co eq1)
1073     co2 = rwi_co eq2
1074
1075 applySubstFam _ _ = return Nothing
1076 \end{code}
1077
1078 Attempt to apply the SubstVarVar rule.  The rule is
1079
1080   co1 :: x ~ t  &  co2 :: x ~ s
1081   =(SubstVarVar)=>
1082   co1 :: x ~ t  &  co2' :: t ~ s with co2 = co1 |> co2'
1083
1084 where co1 may be a wanted only if co2 is a wanted, too.
1085
1086 Returns Nothing if the rule could not be applied.  Otherwise, the equality
1087 co2' is normalised and a list of the normal equalities is returned.  (The
1088 equality co1 is not returned as it remain unaltered.)
1089
1090 \begin{code}
1091 applySubstVarVar :: RewriteInst -> RewriteInst -> TcM (Maybe [RewriteInst])
1092 applySubstVarVar eq1@(RewriteVar {rwi_var = tv1})
1093                  eq2@(RewriteVar {rwi_var = tv2})
1094
1095     -- rule matches => rewrite
1096   | tv1 == tv2 &&
1097     (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
1098   = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
1099        ; eq2' <- deriveEqInst eq2 lhs rhs co2'
1100        ; liftM Just $ normEqInst eq2'
1101        }
1102
1103     -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
1104   | tv1 == tv2 &&
1105     (isWantedRewriteInst eq1 || not (isWantedRewriteInst eq2))
1106   = return $ Just [eq2]
1107
1108   where
1109     lhs = rwi_right eq1
1110     rhs = rwi_right eq2
1111     co1 = eqInstCoType (rwi_co eq1)
1112     co2 = rwi_co eq2
1113
1114 applySubstVarVar _ _ = return Nothing
1115 \end{code}
1116
1117 Attempt to apply the SubstVarFam rule.  The rule is
1118
1119   co1 :: x ~ t  &  co2 :: F s1..sn ~ s
1120   =(SubstVarFam)=>
1121   co1 :: x ~ t  &  co2' :: [t/x](F s1..sn) ~ s
1122     with co2 = [co1/x](F s1..sn) |> co2'
1123
1124 where x occurs in F s1..sn. (co1 may be local or wanted.)
1125
1126 Returns Nothing if the rule could not be applied.  Otherwise, the equality
1127 co2' is returned.  (The equality co1 is not returned as it remain unaltered.)
1128
1129 \begin{code}
1130 applySubstVarFam :: RewriteInst -> RewriteInst -> TcM (Maybe RewriteInst)
1131
1132   -- rule matches => rewrite
1133 applySubstVarFam eq1@(RewriteVar {rwi_var = tv1})
1134                  eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
1135   | tv1 `elemVarSet` tyVarsOfTypes args2
1136   = do { let co1Subst = substTyWith [tv1] [co1] (mkTyConApp fam2 args2)
1137              args2'   = substTysWith [tv1] [rhs1] args2
1138              lhs2     = mkTyConApp fam2 args2'
1139        ; co2' <- mkRightTransEqInstCo co2 co1Subst (lhs2, rhs2)
1140        ; return $ Just (eq2 {rwi_args = args2', rwi_co = co2'})
1141        }
1142   where
1143     rhs1 = rwi_right eq1
1144     rhs2 = rwi_right eq2
1145     co1  = eqInstCoType (rwi_co eq1)
1146     co2  = rwi_co eq2
1147
1148   -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
1149 applySubstVarFam (RewriteFam {rwi_args = args1})
1150                  eq2@(RewriteVar {rwi_var = tv2})
1151   | tv2 `elemVarSet` tyVarsOfTypes args1
1152   = return $ Just eq2
1153
1154 applySubstVarFam _ _ = return Nothing
1155 \end{code}
1156
1157
1158 %************************************************************************
1159 %*                                                                      *
1160                 Finalisation of equalities
1161 %*                                                                      *
1162 %************************************************************************
1163
1164 Exhaustive substitution of all variable equalities of the form co :: x ~ t
1165 (both local and wanted) into the right-hand sides of all other equalities and
1166 of family equalities of the form co :: F t1..tn ~ alpha into both sides of all
1167 other *family* equalities.  This may lead to recursive equalities; i.e., (1)
1168 we need to apply the substitution implied by one equality exhaustively before
1169 turning to the next and (2) we need an occurs check.
1170
1171 We also apply the same substitutions to the local and wanted class and IP
1172 dictionaries.
1173
1174 We perform the substitutions in two steps:
1175
1176   Step A: Substitute variable equalities into the right-hand sides of all
1177           other equalities (but wanted only into wanteds) and into class and IP
1178           constraints (again wanteds only into wanteds).
1179
1180   Step B: Substitute wanted family equalities `co :: F t1..tn ~ alpha', where
1181           'alpha' is a skolem flexible (i.e., not free in the environment),
1182           into the right-hand sides of all wanted variable equalities and into
1183           both sides of all wanted family equalities.
1184
1185   Step C: Substitute the remaining wanted family equalities `co :: F t1..tn ~
1186           alpha' into the right-hand sides of all wanted variable equalities
1187           and into both sides of all wanted family equalities.
1188
1189 In inference mode, we do not substitute into variable equalities in Steps B & C.
1190
1191 The treatment of flexibles in wanteds is quite subtle.  We absolutely want to
1192 substitute variable equalities first; e.g., consider
1193
1194   F s ~ alpha, alpha ~ t
1195
1196 If we don't substitute `alpha ~ t', we may instantiate `t' with `F s' instead.
1197 This would be bad as `F s' is less useful, eg, as an argument to a class
1198 constraint.
1199
1200 The restriction on substituting locals is necessary due to examples, such as
1201
1202   F delta ~ alpha, F alpha ~ delta,
1203
1204 where `alpha' is a skolem flexible and `delta' a environment flexible. We need
1205 to produce `F (F delta) ~ delta' (and not `F (F alpha) ~ alpha'). Otherwise,
1206 we may wrongly claim to having performed an improvement, which can lead to
1207 non-termination of the combined class-family solver.
1208
1209 We do also substitute flexibles, as in `alpha ~ t' into class constraints.
1210 When `alpha' is later instantiated, we'd get the same effect, but in the
1211 meantime the class constraint would miss some information, which would be a
1212 problem in an integrated equality-class solver.
1213
1214 NB:
1215 * Given that we apply the substitution corresponding to a single equality
1216   exhaustively, before turning to the next, and because we eliminate recursive
1217   equalities, all opportunities for subtitution will have been exhausted after
1218   we have considered each equality once.
1219
1220 \begin{code}
1221 substitute :: [RewriteInst]       -- equalities
1222            -> [Inst]              -- local class dictionaries
1223            -> [Inst]              -- wanted class dictionaries
1224            -> Bool                -- True ~ checking mode; False ~ inference
1225            -> TyVarSet            -- flexibles free in the environment
1226            -> TcM ([RewriteInst], -- equalities after substitution
1227                    TcDictBinds,   -- all newly generated dictionary bindings
1228                    [Inst],        -- local dictionaries after substitution
1229                    [Inst])        -- wanted dictionaries after substitution
1230 substitute eqs locals wanteds checkingMode freeFlexibles
1231   = -- We achieve the sequencing of "Step A", "Step B", and "Step C" above by
1232     -- sorting the equalities appropriately: first all variable, then all
1233     -- family/skolem, and then the remaining family equalities.
1234     let (var_eqs, fam_eqs)             = partition isRewriteVar eqs
1235         (fam_skolem_eqs, fam_eqs_rest) = partition isFamSkolemEq fam_eqs
1236     in
1237     subst (var_eqs ++ fam_skolem_eqs ++ fam_eqs_rest) [] emptyBag locals wanteds
1238   where
1239     isFamSkolemEq (RewriteFam {rwi_right = ty})
1240       | Just tv <- tcGetTyVar_maybe ty = not (tv `elemVarSet` freeFlexibles)
1241     isFamSkolemEq _ = False
1242
1243     subst [] res binds locals wanteds
1244       = return (res, binds, locals, wanteds)
1245
1246     -- co :: x ~ t
1247     subst (eq@(RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}):eqs)
1248           res binds locals wanteds
1249       = do { traceTc $ ptext (sLit "TcTyFuns.substitute[RewriteVar]:") <+>
1250                        ppr eq
1251
1252              -- create the substitution
1253            ; let coSubst = zipOpenTvSubst [tv] [eqInstCoType co]
1254                  tySubst = zipOpenTvSubst [tv] [ty]
1255
1256              -- substitute into all other equalities
1257            ; eqs' <- mapM (substEq eq coSubst tySubst) eqs
1258            ; res' <- mapM (substEq eq coSubst tySubst) res
1259
1260              -- only substitute local equalities into local dictionaries
1261            ; (lbinds, locals')  <- if not (isWantedCo co)
1262                                    then
1263                                      mapAndUnzipM
1264                                        (substDict eq coSubst tySubst False)
1265                                        locals
1266                                    else
1267                                      return ([], locals)
1268
1269               -- substitute all equalities into wanteds dictionaries
1270            ; (wbinds, wanteds') <- mapAndUnzipM
1271                                      (substDict eq coSubst tySubst True)
1272                                      wanteds
1273
1274            ; let binds' = unionManyBags $ binds : lbinds ++ wbinds
1275            ; subst eqs' (eq:res') binds' locals' wanteds'
1276            }
1277
1278     -- co ::^w F t1..tn ~ alpha
1279     subst (eq@(RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = ty,
1280                            rwi_co = co}):eqs)
1281           res binds locals wanteds
1282       | Just tv <- tcGetTyVar_maybe ty
1283       , isMetaTyVar tv
1284       , isWantedCo co
1285       = do { traceTc $ ptext (sLit "TcTyFuns.substitute[RewriteFam]:") <+>
1286                        ppr eq
1287
1288              -- create the substitution
1289            ; let coSubst = zipOpenTvSubst [tv] [mkSymCoercion $ eqInstCoType co]
1290                  tySubst = zipOpenTvSubst [tv] [mkTyConApp fam args]
1291
1292              -- substitute into other wanted equalities (`substEq' makes sure
1293              -- that we only substitute into wanteds)
1294            ; eqs' <- mapM (substEq eq coSubst tySubst) eqs
1295            ; res' <- mapM (substEq eq coSubst tySubst) res
1296
1297            ; subst eqs' (eq:res') binds locals wanteds
1298            }
1299
1300     subst (eq:eqs) res binds locals wanteds
1301       = subst eqs (eq:res) binds locals wanteds
1302
1303       -- We have, co :: tv ~ ty
1304       -- => apply [ty/tv] to right-hand side of eq2
1305       --    (but only if tv actually occurs in the right-hand side of eq2
1306       --    and if eq2 is a local, co :: tv ~ ty needs to be a local, too)
1307     substEq (RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co})
1308             coSubst tySubst eq2
1309       |  tv `elemVarSet` tyVarsOfType (rwi_right eq2)
1310       && (isWantedRewriteInst eq2 || not (isWantedCo co))
1311       = do { let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
1312                  right2'  = substTy tySubst (rwi_right eq2)
1313                  left2    = case eq2 of
1314                               RewriteVar {rwi_var = tv2}   -> mkTyVarTy tv2
1315                               RewriteFam {rwi_fam = fam,
1316                                           rwi_args = args} ->mkTyConApp fam args
1317            ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2')
1318            ; case eq2 of
1319                RewriteVar {rwi_var = tv2} | tv2 `elemVarSet` tyVarsOfType ty
1320                  -> occurCheckErr left2 right2'
1321                _ -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
1322            }
1323
1324       -- We have, co ::^w F t1..tn ~ tv
1325       -- => apply [F t1..tn/tv] to eq2
1326       --    (but only if tv actually occurs in eq2
1327       --    and eq2 is a wanted equality
1328       --    and we are either in checking mode or eq2 is a family equality)
1329     substEq (RewriteFam {rwi_args = args, rwi_right = ty})
1330             coSubst tySubst eq2
1331       | Just tv <- tcGetTyVar_maybe ty
1332       , tv `elemVarSet` tyVarsOfRewriteInst eq2
1333       , isWantedRewriteInst eq2
1334       , checkingMode || not (isRewriteVar eq2)
1335       = do { -- substitute into the right-hand side
1336            ; let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
1337                  right2'  = substTy tySubst (rwi_right eq2)
1338                  left2    = case eq2 of
1339                               RewriteVar {rwi_var = tv2}   -> mkTyVarTy tv2
1340                               RewriteFam {rwi_fam = fam,
1341                                           rwi_args = args} -> mkTyConApp fam args
1342            ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2')
1343            ; case eq2 of
1344                RewriteVar {rwi_var = tv2}
1345                  -- variable equality: perform an occurs check
1346                  | tv2 `elemVarSet` tyVarsOfTypes args
1347                  -> occurCheckErr left2 right2'
1348                  | otherwise
1349                  -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
1350                RewriteFam {rwi_fam = fam}
1351                  -- family equality: substitute also into the left-hand side
1352                  -> do { let co1Subst = substTy coSubst left2
1353                              args2'   = substTys tySubst (rwi_args  eq2)
1354                              left2'   = mkTyConApp fam args2'
1355                        ; co2'' <- mkRightTransEqInstCo co2' co1Subst
1356                                                        (left2', right2')
1357                        ; return $ eq2 {rwi_args = args2', rwi_right = right2',
1358                                        rwi_co = co2''}
1359                        }
1360            }
1361
1362       -- unchanged
1363     substEq _ _ _ eq2
1364       = return eq2
1365
1366       -- We have, co :: tv ~ ty
1367       -- => apply [ty/tv] to dictionary predicate
1368       --    (but only if tv actually occurs in the predicate)
1369     substDict (RewriteVar {rwi_var = tv}) coSubst tySubst isWanted dict
1370       | isClassDict dict
1371       , tv `elemVarSet` tyVarsOfPred (tci_pred dict)
1372       = do { let co1Subst = PredTy (substPred coSubst (tci_pred dict))
1373                  pred'    = substPred tySubst (tci_pred dict)
1374            ; (dict', binds) <- mkDictBind dict isWanted co1Subst pred'
1375            ; return (binds, dict')
1376            }
1377
1378       -- unchanged
1379     substDict _ _ _ _ dict
1380       = return (emptyBag, dict)
1381 -- !!!TODO: Still need to substitute into IP constraints.
1382 \end{code}
1383
1384 For any *wanted* variable equality of the form co :: alpha ~ t or co :: a ~
1385 alpha, we record a binding of alpha with t or a, respectively, and for co :=
1386 id.  We do the same for equalities of the form co :: F t1..tn ~ alpha unless
1387 we are in inference mode and alpha appears in the environment - i.e., it is
1388 not a flexible introduced by flattening locals or it is local, but was
1389 propagated into the environment by the instantiation of a variable equality.
1390
1391 We proceed in two phases: (1) first we consider all variable equalities and then
1392 (2) we consider all family equalities.  The two phase structure is required as
1393 the recorded variable equalities determine which skolems flexibles escape, and
1394 hence, which family equalities may be recorded as bindings.
1395
1396 We return all wanted equalities for which we did not generate a binding.
1397 (These can be skolem variable equalities, cyclic variable equalities, and
1398 family equalities.)
1399
1400 We don't update any meta variables.  Instead, instantiation simply implies
1401 putting a type variable binding into the binding pool of TcM.
1402
1403 NB:
1404  * We may encounter filled flexibles due to the instant filling of local
1405    skolems in local-given constraints during flattening.
1406  * Be careful with SigTVs.  They can only be instantiated with other SigTVs or
1407    rigid skolems.
1408
1409 \begin{code}
1410 bindAndExtract :: [RewriteInst] -> Bool -> TyVarSet -> TcM [Inst]
1411 bindAndExtract eqs checkingMode freeFlexibles
1412   = do { traceTc $ hang (ptext (sLit "bindAndExtract:"))
1413                      4 (ppr eqs $$ ppr freeFlexibles)
1414        ; residuals1 <- mapMaybeM instVarEq (filter isWantedRewriteInst eqs)
1415        ; escapingSkolems <- getEscapingSkolems
1416        ; let newFreeFlexibles = freeFlexibles `unionVarSet` escapingSkolems
1417        ; residuals2 <- mapMaybeM (instFamEq newFreeFlexibles) residuals1
1418        ; mapM rewriteInstToInst residuals2
1419        }
1420   where
1421     -- NB: we don't have to transitively chase the relation as the substitution
1422     --     process applied before generating the bindings was exhaustive
1423     getEscapingSkolems
1424       = do { tybinds_rel <- getTcTyVarBindsRelation
1425            ; return (unionVarSets . map snd . filter isFree $ tybinds_rel)
1426            }
1427       where
1428         isFree (tv, _) = tv `elemVarSet` freeFlexibles
1429
1430         -- co :: alpha ~ t or co :: a ~ alpha
1431     instVarEq eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co})
1432       = do { flexi_tv1       <- isFlexible   tv1
1433            ; maybe_flexi_tv2 <- isFlexibleTy ty2
1434            ; case (flexi_tv1, maybe_flexi_tv2) of
1435                (True, Just tv2)
1436                  | isSigTyVar tv1 && isSigTyVar tv2
1437                  -> -- co :: alpha ~ beta, where both a SigTvs
1438                     doInst (rwi_swapped eq) tv1 ty2 co eq
1439                (True, Nothing)
1440                  | Just tv2 <- tcGetTyVar_maybe ty2
1441                  , isSigTyVar tv1
1442                  , isSkolemTyVar tv2
1443                  -> -- co :: alpha ~ a, where alpha is a SigTv
1444                     doInst (rwi_swapped eq) tv1 ty2 co eq
1445                (True, _)
1446                  | not (isSigTyVar tv1)
1447                  -> -- co :: alpha ~ t, where alpha is not a SigTv
1448                     doInst (rwi_swapped eq) tv1 ty2 co eq
1449                (False, Just tv2)
1450                  | isSigTyVar tv2
1451                  , isSkolemTyVar tv1
1452                  -> -- co :: a ~ alpha, where alpha is a SigTv
1453                     doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
1454                  | not (isSigTyVar tv2)
1455                  -> -- co :: a ~ alpha, where alpha is not a SigTv
1456                     --                        ('a' may be filled)
1457                     doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
1458                _ -> return $ Just eq
1459            }
1460     instVarEq eq = return $ Just eq
1461
1462         -- co :: F args ~ alpha,
1463         -- and we are either in checking mode or alpha is a skolem flexible that
1464         --     doesn't escape
1465     instFamEq newFreeFlexibles eq@(RewriteFam {rwi_fam = fam, rwi_args = args,
1466                                                rwi_right = ty2, rwi_co = co})
1467       | Just tv2 <- tcGetTyVar_maybe ty2
1468       , checkingMode || not (tv2 `elemVarSet` newFreeFlexibles)
1469       = do { flexi_tv2 <- isFlexible tv2
1470            ; if flexi_tv2
1471              then
1472                doInst (not $ rwi_swapped eq) tv2 (mkTyConApp fam args) co eq
1473              else
1474                return $ Just eq
1475            }
1476     instFamEq _ eq = return $ Just eq
1477
1478     -- tv is a meta var, but not a SigTV and not filled
1479     isFlexible tv
1480       | isMetaTyVar tv = liftM isFlexi $ readMetaTyVar tv
1481       | otherwise      = return False
1482
1483     -- type is a tv that is a meta var, but not a SigTV and not filled
1484     isFlexibleTy ty
1485       | Just tv <- tcGetTyVar_maybe ty = do {flexi <- isFlexible tv
1486                                             ; if flexi then return $ Just tv
1487                                                        else return Nothing
1488                                             }
1489       | otherwise                      = return Nothing
1490
1491     doInst _swapped _tv _ty (Right ty) _eq
1492       = pprPanic "TcTyFuns.doInst: local eq: " (ppr ty)
1493     doInst swapped tv ty (Left cotv) eq
1494       = do { lookupTV <- lookupTcTyVar tv
1495            ; bMeta swapped tv lookupTV ty cotv
1496            }
1497       where
1498         -- Try to create a binding for a meta variable.  There is *no* need to
1499         -- consider reorienting the underlying equality; `checkOrientation'
1500         -- makes sure that we get variable-variable equalities only in the
1501         -- appropriate orientation.
1502         --
1503         bMeta :: Bool                    -- is this a swapped equality?
1504               -> TcTyVar                 -- tyvar to instantiate
1505               -> LookupTyVarResult       -- lookup result of that tyvar
1506               -> TcType                  -- to to instantiate tyvar with
1507               -> TcTyVar                 -- coercion tyvar of current equality
1508               -> TcM (Maybe RewriteInst) -- returns the original equality if
1509                                          -- the tyvar could not be instantiated,
1510                                          -- and hence, the equality must be kept
1511
1512         -- meta variable has been filled already
1513         -- => this should never happen due to the use of `isFlexible' above
1514         bMeta _swapped tv (IndirectTv fill_ty) ty _cotv
1515           = pprPanic "TcTyFuns.bMeta" $
1516               ptext (sLit "flexible") <+> ppr tv <+>
1517               ptext (sLit "already filled with") <+> ppr fill_ty <+>
1518               ptext (sLit "meant to fill with") <+> ppr ty
1519
1520         -- type variable meets type variable
1521         -- => `checkOrientation' already ensures that it is fine to instantiate
1522         --    tv1 with tv2, but chase tv2's instantiations if necessary, so that
1523         --    we eventually can perform a kinds check in bMetaInst
1524         -- NB: tv's instantiations won't alter the orientation in which we
1525         --     want to instantiate as they either constitute a family
1526         --     application or are themselves due to a properly oriented
1527         --     instantiation
1528         bMeta swapped tv1 details1@(DoneTv (MetaTv _ _)) ty@(TyVarTy tv2) cotv
1529           = do { lookupTV2 <- lookupTcTyVar tv2
1530                ; case lookupTV2 of
1531                    IndirectTv ty' -> bMeta swapped tv1 details1 ty' cotv
1532                    DoneTv _       -> bMetaInst swapped tv1 ty cotv
1533                }
1534
1535         -- updatable meta variable meets non-variable type
1536         -- => occurs check, monotype check, and kinds match check, then bind
1537         bMeta swapped tv (DoneTv (MetaTv _ _ref)) non_tv_ty cotv
1538           = bMetaInst swapped tv non_tv_ty cotv
1539
1540         bMeta _ _ _ _ _ = panic "TcTyFuns.bMeta"
1541
1542         -- We know `tv' can be instantiated; check that `ty' is alright for
1543         -- instantiating `tv' with and then record a binding; we return the
1544         -- original equality if it is cyclic through a synonym family
1545         bMetaInst swapped tv ty cotv
1546           = do {   -- occurs + monotype check
1547                ; mb_ty' <- checkTauTvUpdate tv ty
1548
1549                ; case mb_ty' of
1550                    Nothing  ->
1551                      -- there may be a family in non_tv_ty due to an unzonked,
1552                      -- but updated skolem for a local equality
1553                      -- (cf `wantedToLocal')
1554                      return $ Just eq
1555                    Just ty' ->
1556                      do { checkKinds swapped tv ty'
1557                         ; bindMetaTyVar tv ty'          -- bind meta var
1558                         ; bindMetaTyVar cotv ty'        -- bind co var
1559                         ; return Nothing
1560                         }
1561                }
1562 \end{code}
1563
1564
1565 %************************************************************************
1566 %*                                                                      *
1567 \section{Errors}
1568 %*                                                                      *
1569 %************************************************************************
1570
1571 The infamous couldn't match expected type soandso against inferred type
1572 somethingdifferent message.
1573
1574 \begin{code}
1575 eqInstMisMatch :: Inst -> TcM a
1576 eqInstMisMatch inst
1577   = ASSERT( isEqInst inst )
1578     setErrCtxt ctxt $ failWithMisMatch ty_act ty_exp
1579   where
1580     (ty_act, ty_exp) = eqInstTys inst
1581     InstLoc _ _ ctxt = instLoc   inst
1582
1583 -----------------------
1584 failWithMisMatch :: TcType -> TcType -> TcM a
1585 -- Generate the message when two types fail to match,
1586 -- going to some trouble to make it helpful.
1587 -- The argument order is: actual type, expected type
1588 failWithMisMatch ty_act ty_exp
1589   = do  { env0 <- tcInitTidyEnv
1590         ; ty_exp <- zonkTcType ty_exp
1591         ; ty_act <- zonkTcType ty_act
1592         ; failWithTcM (misMatchMsg env0 (ty_act, ty_exp))
1593         }
1594
1595 misMatchMsg :: TidyEnv -> (TcType, TcType) -> (TidyEnv, SDoc)
1596 misMatchMsg env0 (ty_act, ty_exp)
1597   = let (env1, pp_exp, extra_exp) = ppr_ty env0 ty_exp
1598         (env2, pp_act, extra_act) = ppr_ty env1 ty_act
1599         msg = sep [sep [ptext (sLit "Couldn't match expected type") <+> pp_exp,
1600                         nest 7 $
1601                               ptext (sLit "against inferred type") <+> pp_act],
1602                    nest 2 (extra_exp $$ extra_act),
1603                    nest 2 (vcat (map pp_open_tc (nub open_tcs)))]
1604                         -- See Note [Non-injective type functions]
1605     in
1606     (env2, msg)
1607
1608   where
1609     open_tcs = [tc | TyConApp tc _ <- [ty_act, ty_exp]
1610                    , isOpenTyCon tc ]
1611     pp_open_tc tc = ptext (sLit "NB:") <+> quotes (ppr tc)
1612                     <+> ptext (sLit "is a type function") <> pp_inj
1613         where
1614           pp_inj | isInjectiveTyCon tc = empty
1615                  | otherwise = ptext (sLit (", and may not be injective"))
1616
1617     ppr_ty :: TidyEnv -> TcType -> (TidyEnv, SDoc, SDoc)
1618     ppr_ty env ty
1619       = let (env1, tidy_ty) = tidyOpenType env ty
1620             (env2, extra)  = ppr_extra env1 tidy_ty
1621         in
1622         (env2, quotes (ppr tidy_ty), extra)
1623
1624     -- (ppr_extra env ty) shows extra info about 'ty'
1625     ppr_extra :: TidyEnv -> Type -> (TidyEnv, SDoc)
1626     ppr_extra env (TyVarTy tv)
1627       | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv) && not (isUnk tv)
1628       = (env1, pprSkolTvBinding tv1)
1629       where
1630         (env1, tv1) = tidySkolemTyVar env tv
1631
1632     ppr_extra env _ty = (env, empty)            -- Normal case
1633 \end{code}
1634
1635 Note [Non-injective type functions]
1636 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1637 It's very confusing to get a message like
1638      Couldn't match expected type `Depend s'
1639             against inferred type `Depend s1'
1640 so pp_open_tc adds:
1641        NB: `Depend' is type function, and hence may not be injective
1642
1643 Currently we add this independently for each argument, so we also get
1644      Couldn't match expected type `a'
1645             against inferred type `Dual (Dual a)'
1646        NB: `Dual' is a (non-injective) type function
1647 which is arguably redundant.  But on the other hand, it's probably
1648 a good idea for the programmer to know the error involves type functions
1649 so I've left it in for now.  The obvious alternative is to only add
1650 this NB in the case of matching (T ...) ~ (T ...).
1651
1652
1653 Warn of loopy local equalities that were dropped.
1654
1655 \begin{code}
1656 warnDroppingLoopyEquality :: TcType -> TcType -> TcM ()
1657 warnDroppingLoopyEquality ty1 ty2
1658   = do { env0 <- tcInitTidyEnv
1659        ; ty1 <- zonkTcType ty1
1660        ; ty2 <- zonkTcType ty2
1661        ; let (env1 , tidy_ty1) = tidyOpenType env0 ty1
1662              (_env2, tidy_ty2) = tidyOpenType env1 ty2
1663        ; addWarnTc $ hang (ptext (sLit "Dropping loopy given equality"))
1664                        2 (quotes (ppr tidy_ty1 <+> text "~" <+> ppr tidy_ty2))
1665        }
1666 \end{code}