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 Id
  34 import VarEnv
  35 import VarSet
  36 import Var
  37 import Name
  38 import Bag
  39 import Outputable
  40 import SrcLoc   ( Located(..) )
  41 import Maybes
  42 import FastString
  43
  44 -- standard
  45 import Data.List
  46 import Control.Monad
  47 \end{code}
  48
  49
  50 %************************************************************************
  51 %*                                                                      *
  52                 Normalisation of types wrt toplevel equality schemata
  53 %*                                                                      *
  54 %************************************************************************
  55
  56 Unfold a single synonym family instance and yield the witnessing coercion.
  57 Return 'Nothing' if the given type is either not synonym family instance
  58 or is a synonym family instance that has no matching instance declaration.
  59 (Applies only if the type family application is outermost.)
  60
  61 For example, if we have
  62
  63   :Co:R42T a :: T [a] ~ :R42T a
  64
  65 then 'T [Int]' unfolds to (:R42T Int, :Co:R42T Int).
  66
  67 \begin{code}
  68 tcUnfoldSynFamInst :: Type -> TcM (Maybe (Type, Coercion))
  69 tcUnfoldSynFamInst (TyConApp tycon tys)
  70   | not (isOpenSynTyCon tycon)     -- unfold *only* _synonym_ family instances
  71   = return Nothing
  72   | otherwise
  73   = do { -- we only use the indexing arguments for matching,
  74          -- not the additional ones
  75        ; maybeFamInst <- tcLookupFamInst tycon idxTys
  76        ; case maybeFamInst of
  77            Nothing                -> return Nothing
  78            Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc tys',
  79                                                     mkTyConApp coe_tc tys')
  80              where
  81                tys'   = rep_tys ++ restTys
  82                coe_tc = expectJust "TcTyFuns.tcUnfoldSynFamInst"
  83                                    (tyConFamilyCoercion_maybe rep_tc)
  84        }
  85     where
  86         n                = tyConArity tycon
  87         (idxTys, restTys) = splitAt n tys
  88 tcUnfoldSynFamInst _other = return Nothing
  89 \end{code}
  90
  91 Normalise 'Type's and 'PredType's by unfolding type family applications where
  92 possible (ie, we treat family instances as a TRS).  Also zonk meta variables.
  93
  94         tcNormaliseFamInst ty = (co, ty')
  95         then   co : ty ~ ty'
  96
  97 \begin{code}
  98 -- |Normalise the given type as far as possible with toplevel equalities.
  99 -- This results in a coercion witnessing the type equality, in addition to the
 100 -- normalised type.
 101 --
 102 tcNormaliseFamInst :: TcType -> TcM (CoercionI, TcType)
 103 tcNormaliseFamInst = tcGenericNormaliseFamInst tcUnfoldSynFamInst
 104 \end{code}
 105
 106 Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
 107 apply the normalisation function gives as the first argument to every TyConApp
 108 and every TyVarTy subterm.
 109
 110         tcGenericNormaliseFamInst fun ty = (co, ty')
 111         then   co : ty ~ ty'
 112
 113 This function is (by way of using smart constructors) careful to ensure that
 114 the returned coercion is exactly IdCo (and not some semantically equivalent,
 115 but syntactically different coercion) whenever (ty' `tcEqType` ty).  This
 116 makes it easy for the caller to determine whether the type changed.  BUT
 117 even if we return IdCo, ty' may be *syntactically* different from ty due to
 118 unfolded closed type synonyms (by way of tcCoreView).  In the interest of
 119 good error messages, callers should discard ty' in favour of ty in this case.
 120
 121 \begin{code}
 122 tcGenericNormaliseFamInst :: (TcType -> TcM (Maybe (TcType, Coercion)))
 123                              -- what to do with type functions and tyvars
 124                            -> TcType                    -- old type
 125                            -> TcM (CoercionI, TcType)   -- (coercion, new type)
 126 tcGenericNormaliseFamInst fun ty
 127   | Just ty' <- tcView ty = tcGenericNormaliseFamInst fun ty'
 128 tcGenericNormaliseFamInst fun (TyConApp tyCon tys)
 129   = do  { (cois, ntys) <- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
 130         ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
 131         ; maybe_ty_co <- fun (mkTyConApp tyCon ntys)     -- use normalised args!
 132         ; case maybe_ty_co of
 133             -- a matching family instance exists
 134             Just (ty', co) ->
 135               do { let first_coi = mkTransCoI tycon_coi (ACo co)
 136                  ; (rest_coi, nty) <- tcGenericNormaliseFamInst fun ty'
 137                  ; let fix_coi = mkTransCoI first_coi rest_coi
 138                  ; return (fix_coi, nty)
 139                  }
 140             -- no matching family instance exists
 141             -- we do not do anything
 142             Nothing -> return (tycon_coi, mkTyConApp tyCon ntys)
 143         }
 144 tcGenericNormaliseFamInst fun (AppTy ty1 ty2)
 145   = do  { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
 146         ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
 147         ; return (mkAppTyCoI nty1 coi1 nty2 coi2, mkAppTy nty1 nty2)
 148         }
 149 tcGenericNormaliseFamInst fun (FunTy ty1 ty2)
 150   = do  { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
 151         ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
 152         ; return (mkFunTyCoI nty1 coi1 nty2 coi2, mkFunTy nty1 nty2)
 153         }
 154 tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1)
 155   = do  { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
 156         ; return (mkForAllTyCoI tyvar coi, mkForAllTy tyvar nty1)
 157         }
 158 tcGenericNormaliseFamInst fun ty@(TyVarTy tv)
 159   | isTcTyVar tv
 160   = do  { traceTc (text "tcGenericNormaliseFamInst" <+> ppr ty)
 161         ; res <- lookupTcTyVar tv
 162         ; case res of
 163             DoneTv _ ->
 164               do { maybe_ty' <- fun ty
 165                  ; case maybe_ty' of
 166                      Nothing         -> return (IdCo, ty)
 167                      Just (ty', co1) ->
 168                        do { (coi2, ty'') <- tcGenericNormaliseFamInst fun ty'
 169                           ; return (ACo co1 `mkTransCoI` coi2, ty'')
 170                           }
 171                  }
 172             IndirectTv ty' -> tcGenericNormaliseFamInst fun ty'
 173         }
 174   | otherwise
 175   = return (IdCo, ty)
 176 tcGenericNormaliseFamInst fun (PredTy predty)
 177   = do  { (coi, pred') <- tcGenericNormaliseFamInstPred fun predty
 178         ; return (coi, PredTy pred') }
 179
 180 ---------------------------------
 181 tcGenericNormaliseFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
 182                               -> TcPredType
 183                               -> TcM (CoercionI, TcPredType)
 184
 185 tcGenericNormaliseFamInstPred fun (ClassP cls tys)
 186   = do { (cois, tys')<- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
 187        ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
 188        }
 189 tcGenericNormaliseFamInstPred fun (IParam ipn ty)
 190   = do { (coi, ty') <- tcGenericNormaliseFamInst fun ty
 191        ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
 192        }
 193 tcGenericNormaliseFamInstPred fun (EqPred ty1 ty2)
 194   = do { (coi1, ty1') <- tcGenericNormaliseFamInst fun ty1
 195        ; (coi2, ty2') <- tcGenericNormaliseFamInst fun ty2
 196        ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
 197 \end{code}
 198
 199
 200 %************************************************************************
 201 %*                                                                      *
 202                 Normalisation of instances wrt to equalities
 203 %*                                                                      *
 204 %************************************************************************
 205
 206 \begin{code}
 207 tcReduceEqs :: [Inst]             -- locals
 208             -> [Inst]             -- wanteds
 209             -> TcM ([Inst],       -- normalised locals (w/o equalities)
 210                     [Inst],       -- normalised wanteds (including equalities)
 211                     TcDictBinds,  -- bindings for all simplified dictionaries
 212                     Bool)         -- whether any flexibles where instantiated
 213 tcReduceEqs locals wanteds
 214   = do { let (local_eqs  , local_dicts)   = partition isEqInst locals
 215              (wanteds_eqs, wanteds_dicts) = partition isEqInst wanteds
 216        ; eqCfg1 <- normaliseEqs (local_eqs ++ wanteds_eqs)
 217        ; eqCfg2 <- normaliseDicts False local_dicts
 218        ; eqCfg3 <- normaliseDicts True  wanteds_dicts
 219        ; eqCfg <- propagateEqs (eqCfg1 `unionEqConfig` eqCfg2
 220                                        `unionEqConfig` eqCfg3)
 221        ; finaliseEqsAndDicts eqCfg
 222        }
 223 \end{code}
 224
 225
 226 %************************************************************************
 227 %*                                                                      *
 228                 Equality Configurations
 229 %*                                                                      *
 230 %************************************************************************
 231
 232 We maintain normalised equalities together with the skolems introduced as
 233 intermediates during flattening of equalities as well as
 234
 235 !!!TODO: We probably now can do without the skolem set.  It's not used during
 236 finalisation in the current code.
 237
 238 \begin{code}
 239 -- |Configuration of normalised equalities used during solving.
 240 --
 241 data EqConfig = EqConfig { eqs     :: [RewriteInst]     -- all equalities
 242                          , locals  :: [Inst]            -- given dicts
 243                          , wanteds :: [Inst]            -- wanted dicts
 244                          , binds   :: TcDictBinds       -- bindings
 245                          , skolems :: TyVarSet          -- flattening skolems
 246                          }
 247
 248 addSkolems :: EqConfig -> TyVarSet -> EqConfig
 249 addSkolems eqCfg newSkolems
 250   = eqCfg {skolems = skolems eqCfg `unionVarSet` newSkolems}
 251
 252 addEq :: EqConfig -> RewriteInst -> EqConfig
 253 addEq eqCfg eq = eqCfg {eqs = eq : eqs eqCfg}
 254
 255 unionEqConfig :: EqConfig -> EqConfig -> EqConfig
 256 unionEqConfig eqc1 eqc2 = EqConfig
 257                           { eqs     = eqs eqc1 ++ eqs eqc2
 258                           , locals  = locals eqc1 ++ locals eqc2
 259                           , wanteds = wanteds eqc1 ++ wanteds eqc2
 260                           , binds   = binds eqc1 `unionBags` binds eqc2
 261                           , skolems = skolems eqc1 `unionVarSet` skolems eqc2
 262                           }
 263
 264 emptyEqConfig :: EqConfig
 265 emptyEqConfig = EqConfig
 266                 { eqs     = []
 267                 , locals  = []
 268                 , wanteds = []
 269                 , binds   = emptyBag
 270                 , skolems = emptyVarSet
 271                 }
 272
 273 instance Outputable EqConfig where
 274   ppr (EqConfig {eqs = eqs, locals = locals, wanteds = wanteds, binds = binds})
 275     = vcat [ppr eqs, ppr locals, ppr wanteds, ppr binds]
 276 \end{code}
 277
 278 The set of operations on an equality configuration.  We obtain the initialise
 279 configuration by normalisation ('normaliseEqs'), solve the equalities by
 280 propagation ('propagateEqs'), and eventually finalise the configuration when
 281 no further propoagation is possible.
 282
 283 \begin{code}
 284 -- |Turn a set of equalities into an equality configuration for solving.
 285 --
 286 -- Precondition: The Insts are zonked.
 287 --
 288 normaliseEqs :: [Inst] -> TcM EqConfig
 289 normaliseEqs eqs
 290   = do { ASSERTM2( allM isValidWantedEqInst eqs, ppr eqs )
 291        ; traceTc $ ptext (sLit "Entering normaliseEqs")
 292
 293        ; (eqss, skolemss) <- mapAndUnzipM normEqInst eqs
 294        ; return $ emptyEqConfig { eqs = concat eqss
 295                                 , skolems = unionVarSets skolemss
 296                                 }
 297        }
 298
 299 -- |Flatten the type arguments of all dictionaries, returning the result as a
 300 -- equality configuration.  The dictionaries go into the 'wanted' component if
 301 -- the second argument is 'True'.
 302 --
 303 -- Precondition: The Insts are zonked.
 304 --
 305 normaliseDicts :: Bool -> [Inst] -> TcM EqConfig
 306 normaliseDicts isWanted insts
 307   = do { traceTc $ ptext (sLit "Entering normaliseDicts") <+>
 308                    ptext (if isWanted then sLit "[Wanted]" else sLit "[Local]")
 309        ; (insts', eqss, bindss, skolemss) <- mapAndUnzip4M (normDict isWanted)
 310                                                            insts
 311        ; return $ emptyEqConfig { eqs     = concat eqss
 312                                 , locals  = if isWanted then [] else insts'
 313                                 , wanteds = if isWanted then insts' else []
 314                                 , binds   = unionManyBags bindss
 315                                 , skolems = unionVarSets skolemss
 316                                 }
 317        }
 318
 319 -- |Solves the equalities as far as possible by applying propagation rules.
 320 --
 321 propagateEqs :: EqConfig -> TcM EqConfig
 322 propagateEqs eqCfg@(EqConfig {eqs = todoEqs})
 323   = do { traceTc $ hang (ptext (sLit "Entering propagateEqs:"))
 324                      4 (ppr eqCfg)
 325
 326        ; propagate todoEqs (eqCfg {eqs = []})
 327        }
 328
 329 -- |Finalise a set of equalities and associated dictionaries after
 330 -- propagation.  The returned Boolean value is `True' iff any flexible
 331 -- variables, except those introduced by flattening (i.e., those in the
 332 -- `skolems' component of the argument) where instantiated. The first returned
 333 -- set of instances are the locals (without equalities) and the second set are
 334 -- all residual wanteds, including equalities.
 335 --
 336 -- Remove all identity dictinary bindings (i.e., those whose source and target
 337 -- dictionary are the same).  This is important for termination, as
 338 -- TcSimplify.reduceContext takes the presence of dictionary bindings as an
 339 -- indicator that there was some improvement.
 340 --
 341 finaliseEqsAndDicts :: EqConfig
 342                     -> TcM ([Inst], [Inst], TcDictBinds, Bool)
 343 finaliseEqsAndDicts (EqConfig { eqs     = eqs
 344                               , locals  = locals
 345                               , wanteds = wanteds
 346                               , binds   = binds
 347                               })
 348   = do { traceTc $ ptext (sLit "finaliseEqsAndDicts")
 349        ; (eqs', subst_binds, locals', wanteds') <- substitute eqs locals wanteds
 350        ; (eqs'', improved) <- instantiateAndExtract eqs'
 351        ; final_binds <- filterM nonTrivialDictBind $
 352                           bagToList (subst_binds `unionBags` binds)
 353
 354        ; ASSERTM2( allM isValidWantedEqInst eqs'', ppr eqs'' )
 355        ; return (locals', eqs'' ++ wanteds', listToBag final_binds, improved)
 356        }
 357   where
 358     nonTrivialDictBind (L _ (VarBind { var_id = ide1
 359                                      , var_rhs = L _ (HsWrap _ (HsVar ide2))}))
 360       = do { ty1 <- zonkTcType (idType ide1)
 361            ; ty2 <- zonkTcType (idType ide2)
 362            ; return $ not (ty1 `tcEqType` ty2)
 363            }
 364     nonTrivialDictBind _ = return True
 365 \end{code}
 366
 367
 368 %************************************************************************
 369 %*                                                                      *
 370                 Normalisation of equalities
 371 %*                                                                      *
 372 %************************************************************************
 373
 374 A normal equality is a properly oriented equality with associated coercion
 375 that contains at most one family equality (in its left-hand side) is oriented
 376 such that it may be used as a reqrite rule.  It has one of the following two
 377 forms:
 378
 379 (1) co :: F t1..tn ~ t  (family equalities)
 380 (2) co :: x ~ t         (variable equalities)
 381
 382 Variable equalities fall again in two classes:
 383
 384 (2a) co :: x ~ t, where t is *not* a variable, or
 385 (2b) co :: x ~ y, where x > y.
 386
 387 The types t, t1, ..., tn may not contain any occurrences of synonym
 388 families.  Moreover, in Forms (2) & (3), the left-hand side may not occur in
 389 the right-hand side, and the relation x > y is an arbitrary, but total order
 390 on type variables
 391
 392 !!!TODO: We may need to keep track of swapping for error messages (and to
 393 re-orient on finilisation).
 394
 395 \begin{code}
 396 data RewriteInst
 397   = RewriteVar  -- Form (2) above
 398     { rwi_var     :: TyVar    -- may be rigid or flexible
 399     , rwi_right   :: TcType   -- contains no synonym family applications
 400     , rwi_co      :: EqInstCo -- the wanted or given coercion
 401     , rwi_loc     :: InstLoc
 402     , rwi_name    :: Name     -- no semantic significance (cf. TcRnTypes.EqInst)
 403     , rwi_swapped :: Bool     -- swapped orientation of original EqInst
 404     }
 405   | RewriteFam  -- Forms (1) above
 406     { rwi_fam     :: TyCon    -- synonym family tycon
 407     , rwi_args    :: [Type]   -- contain no synonym family applications
 408     , rwi_right   :: TcType   -- contains no synonym family applications
 409     , rwi_co      :: EqInstCo -- the wanted or given coercion
 410     , rwi_loc     :: InstLoc
 411     , rwi_name    :: Name     -- no semantic significance (cf. TcRnTypes.EqInst)
 412     , rwi_swapped :: Bool     -- swapped orientation of original EqInst
 413     }
 414
 415 isWantedRewriteInst :: RewriteInst -> Bool
 416 isWantedRewriteInst = isWantedCo . rwi_co
 417
 418 rewriteInstToInst :: RewriteInst -> TcM Inst
 419 rewriteInstToInst eq@(RewriteVar {rwi_var = tv})
 420   = deriveEqInst eq (mkTyVarTy tv) (rwi_right eq) (rwi_co eq)
 421 rewriteInstToInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
 422   = deriveEqInst eq (mkTyConApp fam args) (rwi_right eq) (rwi_co eq)
 423
 424 -- Derive an EqInst based from a RewriteInst, possibly swapping the types
 425 -- around.
 426 --
 427 deriveEqInst :: RewriteInst -> TcType -> TcType -> EqInstCo -> TcM Inst
 428 deriveEqInst rewrite ty1 ty2 co
 429   = do { co_adjusted <- if not swapped then return co
 430                                        else mkSymEqInstCo co (ty2, ty1)
 431        ; return $ EqInst
 432                   { tci_left  = left
 433                   , tci_right = right
 434                   , tci_co    = co_adjusted
 435                   , tci_loc   = rwi_loc rewrite
 436                   , tci_name  = rwi_name rewrite
 437                   }
 438        }
 439   where
 440     swapped       = rwi_swapped rewrite
 441     (left, right) = if not swapped then (ty1, ty2) else (ty2, ty1)
 442
 443 instance Outputable RewriteInst where
 444   ppr (RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = rhs, rwi_co =co})
 445     = hsep [ ppr co <+> text "::"
 446            , ppr (mkTyConApp fam args)
 447            , text "~>"
 448            , ppr rhs
 449            ]
 450   ppr (RewriteVar {rwi_var = tv, rwi_right = rhs, rwi_co =co})
 451     = hsep [ ppr co <+> text "::"
 452            , ppr tv
 453            , text "~>"
 454            , ppr rhs
 455            ]
 456 \end{code}
 457
 458 The following functions turn an arbitrary equality into a set of normal
 459 equalities.  This implements the WFlat and LFlat rules of the paper in one
 460 sweep.  However, we use flexible variables for both locals and wanteds, and
 461 avoid to carry around the unflattening substitution \Sigma (for locals) by
 462 already updating the skolems for locals with the family application that they
 463 represent - i.e., they will turn into that family application on the next
 464 zonking (which only happens after finalisation).
 465
 466 In a corresponding manner, normDict normalises class dictionaries by
 467 extracting any synonym family applications and generation appropriate normal
 468 equalities.
 469
 470 Whenever we encounter a loopy equality (of the form a ~ T .. (F ...a...) ...),
 471 we drop that equality and raise an error if it is a wanted or a warning if it
 472 is a local.
 473
 474 \begin{code}
 475 normEqInst :: Inst -> TcM ([RewriteInst], TyVarSet)
 476 -- Normalise one equality.
 477 normEqInst inst
 478   = ASSERT( isEqInst inst )
 479     go ty1 ty2 (eqInstCoercion inst)
 480   where
 481     (ty1, ty2) = eqInstTys inst
 482
 483       -- look through synonyms
 484     go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
 485     go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
 486
 487       -- left-to-right rule with type family head
 488     go (TyConApp con args) ty2 co
 489       | isOpenSynTyCon con
 490       = mkRewriteFam False con args ty2 co
 491
 492       -- right-to-left rule with type family head
 493     go ty1 ty2@(TyConApp con args) co
 494       | isOpenSynTyCon con
 495       = do { co' <- mkSymEqInstCo co (ty2, ty1)
 496            ; mkRewriteFam True con args ty1 co'
 497            }
 498
 499       -- no outermost family
 500     go ty1 ty2 co
 501       = do { (ty1', co1, ty1_eqs, ty1_skolems) <- flattenType inst ty1
 502            ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2
 503            ; let ty12_eqs  = ty1_eqs ++ ty2_eqs
 504                  sym_co2   = mkSymCoercion co2
 505                  eqTys     = (ty1', ty2')
 506            ; (co', ty12_eqs') <- adjustCoercions co co1 sym_co2 eqTys ty12_eqs
 507            ; eqs <- checkOrientation ty1' ty2' co' inst
 508            ; if isLoopyEquality eqs ty12_eqs'
 509              then do { if isWantedCo (tci_co inst)
 510                        then
 511                           addErrCtxt (ptext (sLit "Rejecting loopy equality")) $
 512                             eqInstMisMatch inst
 513                        else
 514                          warnDroppingLoopyEquality ty1 ty2
 515                      ; return ([], emptyVarSet)         -- drop the equality
 516                      }
 517              else
 518                return (eqs ++ ty12_eqs',
 519                       ty1_skolems `unionVarSet` ty2_skolems)
 520            }
 521
 522     mkRewriteFam swapped con args ty2 co
 523       = do { (args', cargs, args_eqss, args_skolemss)
 524                <- mapAndUnzip4M (flattenType inst) args
 525            ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2
 526            ; let co1       = mkTyConApp con cargs
 527                  sym_co2   = mkSymCoercion co2
 528                  all_eqs   = concat args_eqss ++ ty2_eqs
 529                  eqTys     = (mkTyConApp con args', ty2')
 530            ; (co', all_eqs') <- adjustCoercions co co1 sym_co2 eqTys all_eqs
 531            ; let thisRewriteFam = RewriteFam
 532                                   { rwi_fam     = con
 533                                   , rwi_args    = args'
 534                                   , rwi_right   = ty2'
 535                                   , rwi_co      = co'
 536                                   , rwi_loc     = tci_loc inst
 537                                   , rwi_name    = tci_name inst
 538                                   , rwi_swapped = swapped
 539                                   }
 540            ; return $ (thisRewriteFam : all_eqs',
 541                        unionVarSets (ty2_skolems:args_skolemss))
 542            }
 543
 544     -- If the original equality has the form a ~ T .. (F ...a...) ..., we will
 545     -- have a variable equality with 'a' on the lhs as the first equality.
 546     -- Then, check whether 'a' occurs in the lhs of any family equality
 547     -- generated by flattening.
 548     isLoopyEquality (RewriteVar {rwi_var = tv}:_) eqs
 549       = any inRewriteFam eqs
 550       where
 551         inRewriteFam (RewriteFam {rwi_args = args})
 552           = tv `elemVarSet` tyVarsOfTypes args
 553         inRewriteFam _ = False
 554     isLoopyEquality _ _ = False
 555
 556 normDict :: Bool -> Inst -> TcM (Inst, [RewriteInst], TcDictBinds, TyVarSet)
 557 -- Normalise one dictionary or IP constraint.
 558 normDict isWanted inst@(Dict {tci_pred = ClassP clas args})
 559   = do { (args', cargs, args_eqss, args_skolemss)
 560            <- mapAndUnzip4M (flattenType inst) args
 561        ; let rewriteCo = PredTy $ ClassP clas cargs
 562              eqs       = concat args_eqss
 563              pred'     = ClassP clas args'
 564        ; if null eqs
 565          then  -- don't generate a binding if there is nothing to flatten
 566            return (inst, [], emptyBag, emptyVarSet)
 567          else do {
 568        ; (inst', bind) <- mkDictBind inst isWanted rewriteCo pred'
 569        ; eqs' <- if isWanted then return eqs else mapM wantedToLocal eqs
 570        ; return (inst', eqs', bind, unionVarSets args_skolemss)
 571        }}
 572 normDict _isWanted inst
 573   = return (inst, [], emptyBag, emptyVarSet)
 574 -- !!!TODO: Still need to normalise IP constraints.
 575
 576 checkOrientation :: Type -> Type -> EqInstCo -> Inst -> TcM [RewriteInst]
 577 -- Performs the occurs check, decomposition, and proper orientation
 578 -- (returns a singleton, or an empty list in case of a trivial equality)
 579 -- NB: We cannot assume that the two types already have outermost type
 580 --     synonyms expanded due to the recursion in the case of type applications.
 581 checkOrientation ty1 ty2 co inst
 582   = go ty1 ty2
 583   where
 584       -- look through synonyms
 585     go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
 586     go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
 587
 588       -- identical types => trivial
 589     go ty1 ty2
 590       | ty1 `tcEqType` ty2
 591       = do { mkIdEqInstCo co ty1
 592            ; return []
 593            }
 594
 595       -- two tvs, left greater => unchanged
 596     go ty1@(TyVarTy tv1) ty2@(TyVarTy tv2)
 597       | tv1 > tv2
 598       = mkRewriteVar False tv1 ty2 co
 599
 600       -- two tvs, right greater => swap
 601       | otherwise
 602       = do { co' <- mkSymEqInstCo co (ty2, ty1)
 603            ; mkRewriteVar True tv2 ty1 co'
 604            }
 605
 606       -- only lhs is a tv => unchanged
 607     go ty1@(TyVarTy tv1) ty2
 608       | ty1 `tcPartOfType` ty2      -- occurs check!
 609       = occurCheckErr ty1 ty2
 610       | otherwise
 611       = mkRewriteVar False tv1 ty2 co
 612
 613       -- only rhs is a tv => swap
 614     go ty1 ty2@(TyVarTy tv2)
 615       | ty2 `tcPartOfType` ty1      -- occurs check!
 616       = occurCheckErr ty2 ty1
 617       | otherwise
 618       = do { co' <- mkSymEqInstCo co (ty2, ty1)
 619            ; mkRewriteVar True tv2 ty1 co'
 620            }
 621
 622       -- type applications => decompose
 623     go ty1 ty2
 624       | Just (ty1_l, ty1_r) <- repSplitAppTy_maybe ty1   -- won't split fam apps
 625       , Just (ty2_l, ty2_r) <- repSplitAppTy_maybe ty2
 626       = do { (co_l, co_r) <- mkAppEqInstCo co (ty1_l, ty2_l) (ty1_r, ty2_r)
 627            ; eqs_l <- checkOrientation ty1_l ty2_l co_l inst
 628            ; eqs_r <- checkOrientation ty1_r ty2_r co_r inst
 629            ; return $ eqs_l ++ eqs_r
 630            }
 631 -- !!!TODO: would be more efficient to handle the FunApp and the data
 632 -- constructor application explicitly.
 633
 634       -- inconsistency => type error
 635     go ty1 ty2
 636       = ASSERT( (not . isForAllTy $ ty1) && (not . isForAllTy $ ty2) )
 637         eqInstMisMatch inst
 638
 639     mkRewriteVar swapped tv ty co = return [RewriteVar
 640                                             { rwi_var     = tv
 641                                             , rwi_right   = ty
 642                                             , rwi_co      = co
 643                                             , rwi_loc     = tci_loc inst
 644                                             , rwi_name    = tci_name inst
 645                                             , rwi_swapped = swapped
 646                                             }]
 647
 648 flattenType :: Inst     -- context to get location  & name
 649             -> Type     -- the type to flatten
 650             -> TcM (Type,           -- the flattened type
 651                     Coercion,       -- coercion witness of flattening wanteds
 652                     [RewriteInst],  -- extra equalities
 653                     TyVarSet)       -- new intermediate skolems
 654 -- Removes all family synonyms from a type by moving them into extra equalities
 655 flattenType inst ty
 656   = go ty
 657   where
 658       -- look through synonyms
 659     go ty | Just ty' <- tcView ty
 660       = do { (ty_flat, co, eqs, skolems) <- go ty'
 661            ; if null eqs
 662              then     -- unchanged, keep the old type with folded synonyms
 663                return (ty, ty, [], emptyVarSet)
 664              else
 665                return (ty_flat, co, eqs, skolems)
 666            }
 667
 668       -- type variable => nothing to do
 669     go ty@(TyVarTy _)
 670       = return (ty, ty, [] , emptyVarSet)
 671
 672       -- type family application
 673       -- => flatten to "gamma :: F t1'..tn' ~ alpha" (alpha & gamma fresh)
 674     go ty@(TyConApp con args)
 675       | isOpenSynTyCon con
 676       = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args
 677            ; alpha <- newFlexiTyVar (typeKind ty)
 678            ; let alphaTy = mkTyVarTy alpha
 679            ; cotv <- newMetaCoVar (mkTyConApp con args') alphaTy
 680            ; let thisRewriteFam = RewriteFam
 681                                   { rwi_fam     = con
 682                                   , rwi_args    = args'
 683                                   , rwi_right   = alphaTy
 684                                   , rwi_co      = mkWantedCo cotv
 685                                   , rwi_loc     = tci_loc inst
 686                                   , rwi_name    = tci_name inst
 687                                   , rwi_swapped = True
 688                                   }
 689            ; return (alphaTy,
 690                      mkTyConApp con cargs `mkTransCoercion` mkTyVarTy cotv,
 691                      thisRewriteFam : concat args_eqss,
 692                      unionVarSets args_skolemss `extendVarSet` alpha)
 693            }           -- adding new unflatten var inst
 694
 695       -- data constructor application => flatten subtypes
 696       -- NB: Special cased for efficiency - could be handled as type application
 697     go ty@(TyConApp con args)
 698       = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args
 699            ; if null args_eqss
 700              then     -- unchanged, keep the old type with folded synonyms
 701                return (ty, ty, [], emptyVarSet)
 702              else
 703                return (mkTyConApp con args',
 704                        mkTyConApp con cargs,
 705                        concat args_eqss,
 706                        unionVarSets args_skolemss)
 707            }
 708
 709       -- function type => flatten subtypes
 710       -- NB: Special cased for efficiency - could be handled as type application
 711     go ty@(FunTy ty_l ty_r)
 712       = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l
 713            ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r
 714            ; if null eqs_l && null eqs_r
 715              then     -- unchanged, keep the old type with folded synonyms
 716                return (ty, ty, [], emptyVarSet)
 717              else
 718                return (mkFunTy ty_l' ty_r',
 719                        mkFunTy co_l co_r,
 720                        eqs_l ++ eqs_r,
 721                        skolems_l `unionVarSet` skolems_r)
 722            }
 723
 724       -- type application => flatten subtypes
 725     go ty@(AppTy ty_l ty_r)
 726       = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l
 727            ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r
 728            ; if null eqs_l && null eqs_r
 729              then     -- unchanged, keep the old type with folded synonyms
 730                return (ty, ty, [], emptyVarSet)
 731              else
 732                return (mkAppTy ty_l' ty_r',
 733                        mkAppTy co_l co_r,
 734                        eqs_l ++ eqs_r,
 735                        skolems_l `unionVarSet` skolems_r)
 736            }
 737
 738       -- forall type => panic if the body contains a type family
 739       -- !!!TODO: As long as the family does not contain a quantified variable
 740       --          we might pull it out, but what if it does contain a quantified
 741       --          variable???
 742     go ty@(ForAllTy _ body)
 743       | null (tyFamInsts body)
 744       = return (ty, ty, [] , emptyVarSet)
 745       | otherwise
 746       = panic "TcTyFuns.flattenType: synonym family in a rank-n type"
 747
 748       -- we should never see a predicate type
 749     go (PredTy _)
 750       = panic "TcTyFuns.flattenType: unexpected PredType"
 751
 752 adjustCoercions :: EqInstCo            -- coercion of original equality
 753                 -> Coercion            -- coercion witnessing the left rewrite
 754                 -> Coercion            -- coercion witnessing the right rewrite
 755                 -> (Type, Type)        -- types of flattened equality
 756                 -> [RewriteInst]       -- equalities from flattening
 757                 -> TcM (EqInstCo,      -- coercion for flattened equality
 758                         [RewriteInst]) -- final equalities from flattening
 759 -- Depending on whether we flattened a local or wanted equality, that equality's
 760 -- coercion and that of the new equalities produced during flattening are
 761 -- adjusted .
 762 adjustCoercions (Left cotv) co1 co2 (ty_l, ty_r) all_eqs
 763     -- wanted => generate a fresh coercion variable for the flattened equality
 764   = do { cotv' <- newMetaCoVar ty_l ty_r
 765        ; writeMetaTyVar cotv $
 766            (co1 `mkTransCoercion` TyVarTy cotv' `mkTransCoercion` co2)
 767        ; return (Left cotv', all_eqs)
 768        }
 769
 770 adjustCoercions co@(Right _) _co1 _co2 _eqTys all_eqs
 771     -- local => turn all new equalities into locals and update (but not zonk)
 772     --          the skolem
 773   = do { all_eqs' <- mapM wantedToLocal all_eqs
 774        ; return (co, all_eqs')
 775        }
 776
 777 mkDictBind :: Inst                 -- original instance
 778            -> Bool                 -- is this a wanted contraint?
 779            -> Coercion             -- coercion witnessing the rewrite
 780            -> PredType             -- coerced predicate
 781            -> TcM (Inst,           -- new inst
 782                    TcDictBinds)    -- binding for coerced dictionary
 783 mkDictBind dict isWanted rewriteCo pred
 784   = do { dict' <- newDictBndr loc pred
 785          -- relate the old inst to the new one
 786          -- target_dict = source_dict `cast` st_co
 787        ; let (target_dict, source_dict, st_co)
 788                | isWanted  = (dict,  dict', mkSymCoercion rewriteCo)
 789                | otherwise = (dict', dict,  rewriteCo)
 790                  -- we have
 791                  --   co :: dict ~ dict'
 792                  -- hence, if isWanted
 793                  --       dict  = dict' `cast` sym co
 794                  --        else
 795                  --       dict' = dict  `cast` co
 796              expr      = HsVar $ instToId source_dict
 797              cast_expr = HsWrap (WpCast st_co) expr
 798              rhs       = L (instLocSpan loc) cast_expr
 799              binds     = instToDictBind target_dict rhs
 800        ; return (dict', binds)
 801        }
 802   where
 803     loc = tci_loc dict
 804
 805 -- gamma :: Fam args ~ alpha
 806 -- => alpha :: Fam args ~ alpha, with alpha := Fam args
 807 --    (the update of alpha will not be apparent during propagation, as we
 808 --    never follow the indirections of meta variables; it will be revealed
 809 --    when the equality is zonked)
 810 wantedToLocal :: RewriteInst -> TcM RewriteInst
 811 wantedToLocal eq@(RewriteFam {rwi_fam   = fam,
 812                               rwi_args  = args,
 813                               rwi_right = alphaTy@(TyVarTy alpha)})
 814   = do { writeMetaTyVar alpha (mkTyConApp fam args)
 815        ; return $ eq {rwi_co = mkGivenCo alphaTy}
 816        }
 817 wantedToLocal _ = panic "TcTyFuns.wantedToLocal"
 818 \end{code}
 819
 820
 821 %************************************************************************
 822 %*                                                                      *
 823                 Propagation of equalities
 824 %*                                                                      *
 825 %************************************************************************
 826
 827 Apply the propagation rules exhaustively.
 828
 829 \begin{code}
 830 propagate :: [RewriteInst] -> EqConfig -> TcM EqConfig
 831 propagate []       eqCfg = return eqCfg
 832 propagate (eq:eqs) eqCfg
 833   = do { optEqs <- applyTop eq
 834        ; case optEqs of
 835
 836               -- Top applied to 'eq' => retry with new equalities
 837            Just (eqs2, skolems2)
 838              -> propagate (eqs2 ++ eqs) (eqCfg `addSkolems` skolems2)
 839
 840               -- Top doesn't apply => try subst rules with all other
 841               --   equalities, after that 'eq' can go into the residual list
 842            Nothing
 843              -> do { (eqs', eqCfg') <- applySubstRules eq eqs eqCfg
 844                    ; propagate eqs' (eqCfg' `addEq` eq)
 845                    }
 846    }
 847
 848 applySubstRules :: RewriteInst                    -- currently considered eq
 849                 -> [RewriteInst]                  -- todo eqs list
 850                 -> EqConfig                       -- residual
 851                 -> TcM ([RewriteInst], EqConfig)  -- new todo & residual
 852 applySubstRules eq todoEqs (eqConfig@EqConfig {eqs = resEqs})
 853   = do { (newEqs_t, unchangedEqs_t, skolems_t) <- mapSubstRules eq todoEqs
 854        ; (newEqs_r, unchangedEqs_r, skolems_r) <- mapSubstRules eq resEqs
 855        ; return (newEqs_t ++ newEqs_r ++ unchangedEqs_t,
 856                  eqConfig {eqs = unchangedEqs_r}
 857                    `addSkolems` (skolems_t `unionVarSet` skolems_r))
 858        }
 859
 860 mapSubstRules :: RewriteInst     -- try substituting this equality
 861               -> [RewriteInst]   -- into these equalities
 862               -> TcM ([RewriteInst], [RewriteInst], TyVarSet)
 863 mapSubstRules eq eqs
 864   = do { (newEqss, unchangedEqss, skolemss) <- mapAndUnzip3M (substRules eq) eqs
 865        ; return (concat newEqss, concat unchangedEqss, unionVarSets skolemss)
 866        }
 867   where
 868     substRules eq1 eq2
 869       = do {   -- try the SubstFam rule
 870              optEqs <- applySubstFam eq1 eq2
 871            ; case optEqs of
 872                Just (eqs, skolems) -> return (eqs, [], skolems)
 873                Nothing             -> do
 874            {   -- try the SubstVarVar rule
 875              optEqs <- applySubstVarVar eq1 eq2
 876            ; case optEqs of
 877                Just (eqs, skolems) -> return (eqs, [], skolems)
 878                Nothing             -> do
 879            {   -- try the SubstVarFam rule
 880              optEqs <- applySubstVarFam eq1 eq2
 881            ; case optEqs of
 882                Just eq -> return ([eq], [], emptyVarSet)
 883                Nothing -> return ([], [eq2], emptyVarSet)
 884                  -- if no rule matches, we return the equlity we tried to
 885                  -- substitute into unchanged
 886            }}}
 887 \end{code}
 888
 889 Attempt to apply the Top rule.  The rule is
 890
 891   co :: F t1..tn ~ t
 892   =(Top)=>
 893   co' :: [s1/x1, .., sm/xm]s ~ t with co = g s1..sm |> co'
 894
 895 where g :: forall x1..xm. F u1..um ~ s and [s1/x1, .., sm/xm]u1 == t1.
 896
 897 Returns Nothing if the rule could not be applied.  Otherwise, the resulting
 898 equality is normalised and a list of the normal equalities is returned.
 899
 900 \begin{code}
 901 applyTop :: RewriteInst -> TcM (Maybe ([RewriteInst], TyVarSet))
 902
 903 applyTop eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
 904   = do { optTyCo <- tcUnfoldSynFamInst (TyConApp fam args)
 905        ; case optTyCo of
 906            Nothing                -> return Nothing
 907            Just (lhs, rewrite_co)
 908              -> do { co' <- mkRightTransEqInstCo co rewrite_co (lhs, rhs)
 909                    ; eq' <- deriveEqInst eq lhs rhs co'
 910                    ; liftM Just $ normEqInst eq'
 911                    }
 912        }
 913   where
 914     co  = rwi_co eq
 915     rhs = rwi_right eq
 916
 917 applyTop _ = return Nothing
 918 \end{code}
 919
 920 Attempt to apply the SubstFam rule.  The rule is
 921
 922   co1 :: F t1..tn ~ t  &  co2 :: F t1..tn ~ s
 923   =(SubstFam)=>
 924   co1 :: F t1..tn ~ t  &  co2' :: t ~ s with co2 = co1 |> co2'
 925
 926 where co1 may be a wanted only if co2 is a wanted, too.
 927
 928 Returns Nothing if the rule could not be applied.  Otherwise, the equality
 929 co2' is normalised and a list of the normal equalities is returned.  (The
 930 equality co1 is not returned as it remain unaltered.)
 931
 932 \begin{code}
 933 applySubstFam :: RewriteInst
 934               -> RewriteInst
 935               -> TcM (Maybe ([RewriteInst], TyVarSet))
 936 applySubstFam eq1@(RewriteFam {rwi_fam = fam1, rwi_args = args1})
 937               eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
 938   | fam1 == fam2 && tcEqTypes args1 args2 &&
 939     (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
 940 -- !!!TODO: tcEqTypes is insufficient as it does not look through type synonyms
 941 -- !!!Check whether anything breaks by making tcEqTypes look through synonyms.
 942 -- !!!Should be ok and we don't want three type equalities.
 943   = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
 944        ; eq2' <- deriveEqInst eq2 lhs rhs co2'
 945        ; liftM Just $ normEqInst eq2'
 946        }
 947   where
 948     lhs = rwi_right eq1
 949     rhs = rwi_right eq2
 950     co1 = eqInstCoType (rwi_co eq1)
 951     co2 = rwi_co eq2
 952 applySubstFam _ _ = return Nothing
 953 \end{code}
 954
 955 Attempt to apply the SubstVarVar rule.  The rule is
 956
 957   co1 :: x ~ t  &  co2 :: x ~ s
 958   =(SubstVarVar)=>
 959   co1 :: x ~ t  &  co2' :: t ~ s with co2 = co1 |> co2'
 960
 961 where co1 may be a wanted only if co2 is a wanted, too.
 962
 963 Returns Nothing if the rule could not be applied.  Otherwise, the equality
 964 co2' is normalised and a list of the normal equalities is returned.  (The
 965 equality co1 is not returned as it remain unaltered.)
 966
 967 \begin{code}
 968 applySubstVarVar :: RewriteInst
 969                  -> RewriteInst
 970                  -> TcM (Maybe ([RewriteInst], TyVarSet))
 971 applySubstVarVar eq1@(RewriteVar {rwi_var = tv1})
 972                  eq2@(RewriteVar {rwi_var = tv2})
 973   | tv1 == tv2 &&
 974     (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
 975   = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
 976        ; eq2' <- deriveEqInst eq2 lhs rhs co2'
 977        ; liftM Just $ normEqInst eq2'
 978        }
 979   where
 980     lhs = rwi_right eq1
 981     rhs = rwi_right eq2
 982     co1 = eqInstCoType (rwi_co eq1)
 983     co2 = rwi_co eq2
 984 applySubstVarVar _ _ = return Nothing
 985 \end{code}
 986
 987 Attempt to apply the SubstVarFam rule.  The rule is
 988
 989   co1 :: x ~ t  &  co2 :: F s1..sn ~ s
 990   =(SubstVarFam)=>
 991   co1 :: x ~ t  &  co2' :: [t/x](F s1..sn) ~ s
 992     with co2 = [co1/x](F s1..sn) |> co2'
 993
 994 where x occurs in F s1..sn. (co1 may be local or wanted.)
 995
 996 Returns Nothing if the rule could not be applied.  Otherwise, the equality
 997 co2' is returned.  (The equality co1 is not returned as it remain unaltered.)
 998
 999 \begin{code}
1000 applySubstVarFam :: RewriteInst -> RewriteInst -> TcM (Maybe RewriteInst)
1001 applySubstVarFam eq1@(RewriteVar {rwi_var = tv1})
1002                  eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
1003   | tv1 `elemVarSet` tyVarsOfTypes args2
1004   = do { let co1Subst = substTyWith [tv1] [co1] (mkTyConApp fam2 args2)
1005              args2'   = substTysWith [tv1] [rhs1] args2
1006              lhs2     = mkTyConApp fam2 args2'
1007        ; co2' <- mkRightTransEqInstCo co2 co1Subst (lhs2, rhs2)
1008        ; return $ Just (eq2 {rwi_args = args2', rwi_co = co2'})
1009        }
1010   where
1011     rhs1 = rwi_right eq1
1012     rhs2 = rwi_right eq2
1013     co1  = eqInstCoType (rwi_co eq1)
1014     co2  = rwi_co eq2
1015 applySubstVarFam _ _ = return Nothing
1016 \end{code}
1017
1018
1019 %************************************************************************
1020 %*                                                                      *
1021                 Finalisation of equalities
1022 %*                                                                      *
1023 %************************************************************************
1024
1025 Exhaustive substitution of all variable equalities of the form co :: x ~ t
1026 (both local and wanted) into the left-hand sides of all other equalities.  This
1027 may lead to recursive equalities; i.e., (1) we need to apply the substitution
1028 implied by one variable equality exhaustively before turning to the next and
1029 (2) we need an occurs check.
1030
1031 We also apply the same substitutions to the local and wanted class and IP
1032 dictionaries.
1033
1034 NB: Given that we apply the substitution corresponding to a single equality
1035 exhaustively, before turning to the next, and because we eliminate recursive
1036 equalities, all opportunities for subtitution will have been exhausted after
1037 we have considered each equality once.
1038
1039 \begin{code}
1040 substitute :: [RewriteInst]       -- equalities
1041            -> [Inst]              -- local class dictionaries
1042            -> [Inst]              -- wanted class dictionaries
1043            -> TcM ([RewriteInst], -- equalities after substitution
1044                    TcDictBinds,   -- all newly generated dictionary bindings
1045                    [Inst],        -- local dictionaries after substitution
1046                    [Inst])        -- wanted dictionaries after substitution
1047 substitute eqs locals wanteds = subst eqs [] emptyBag locals wanteds
1048   where
1049     subst [] res binds locals wanteds
1050       = return (res, binds, locals, wanteds)
1051     subst (eq@(RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}):eqs)
1052           res binds locals wanteds
1053       = do { traceTc $ ptext (sLit "TcTyFuns.substitute:") <+> ppr tv <+>
1054                        ptext (sLit "->") <+> ppr ty
1055            ; let coSubst = zipOpenTvSubst [tv] [eqInstCoType co]
1056                  tySubst = zipOpenTvSubst [tv] [ty]
1057            ; eqs'               <- mapM (substEq eq coSubst tySubst) eqs
1058            ; res'               <- mapM (substEq eq coSubst tySubst) res
1059            ; (lbinds, locals')  <- mapAndUnzipM
1060                                      (substDict eq coSubst tySubst False)
1061                                      locals
1062            ; (wbinds, wanteds') <- mapAndUnzipM
1063                                      (substDict eq coSubst tySubst True)
1064                                      wanteds
1065            ; let binds' = unionManyBags $ binds : lbinds ++ wbinds
1066            ; subst eqs' (eq:res') binds' locals' wanteds'
1067            }
1068     subst (eq:eqs) res binds locals wanteds
1069       = subst eqs (eq:res) binds locals wanteds
1070
1071       -- We have, co :: tv ~ ty
1072       -- => apply [ty/tv] to right-hand side of eq2
1073       --    (but only if tv actually occurs in the right-hand side of eq2)
1074     substEq (RewriteVar {rwi_var = tv, rwi_right = ty})
1075             coSubst tySubst eq2
1076       | tv `elemVarSet` tyVarsOfType (rwi_right eq2)
1077       = do { let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
1078                  right2'  = substTy tySubst (rwi_right eq2)
1079                  left2    = case eq2 of
1080                               RewriteVar {rwi_var = tv2}   -> mkTyVarTy tv2
1081                               RewriteFam {rwi_fam = fam,
1082                                           rwi_args = args} ->mkTyConApp fam args
1083            ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2')
1084            ; case eq2 of
1085                RewriteVar {rwi_var = tv2} | tv2 `elemVarSet` tyVarsOfType ty
1086                  -> occurCheckErr left2 right2'
1087                _ -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
1088            }
1089
1090       -- unchanged
1091     substEq _ _ _ eq2
1092       = return eq2
1093
1094       -- We have, co :: tv ~ ty
1095       -- => apply [ty/tv] to dictionary predicate
1096       --    (but only if tv actually occurs in the predicate)
1097     substDict (RewriteVar {rwi_var = tv})
1098               coSubst tySubst isWanted dict
1099       | isClassDict dict
1100       , tv `elemVarSet` tyVarsOfPred (tci_pred dict)
1101       = do { let co1Subst = PredTy (substPred coSubst (tci_pred dict))
1102                  pred'    = substPred tySubst (tci_pred dict)
1103            ; (dict', binds) <- mkDictBind dict isWanted co1Subst pred'
1104            ; return (binds, dict')
1105            }
1106
1107       -- unchanged
1108     substDict _ _ _ _ dict
1109       = return (emptyBag, dict)
1110 -- !!!TODO: Still need to substitute into IP constraints.
1111 \end{code}
1112
1113 For any *wanted* variable equality of the form co :: alpha ~ t or co :: a ~
1114 alpha, we instantiate alpha with t or a, respectively, and set co := id.
1115 Return all remaining wanted equalities.  The Boolean result component is True
1116 if at least one instantiation of a flexible was performed.
1117
1118 \begin{code}
1119 instantiateAndExtract :: [RewriteInst] -> TcM ([Inst], Bool)
1120 instantiateAndExtract eqs
1121   = do { let wanteds = filter (isWantedCo . rwi_co) eqs
1122        ; wanteds' <- mapM inst wanteds
1123        ; let residuals = catMaybes wanteds'
1124              improved  = length wanteds /= length residuals
1125        ; residuals' <- mapM rewriteInstToInst residuals
1126        ; return (residuals', improved)
1127        }
1128   where
1129     inst eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co})
1130
1131         -- co :: alpha ~ t
1132       | isMetaTyVar tv1
1133       = doInst (rwi_swapped eq) tv1 ty2 co eq
1134
1135         -- co :: a ~ alpha
1136       | Just tv2 <- tcGetTyVar_maybe ty2
1137       , isMetaTyVar tv2
1138       = doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
1139
1140     inst eq = return $ Just eq
1141
1142     doInst _swapped _tv _ty (Right ty) _eq
1143       = pprPanic "TcTyFuns.doInst: local eq: " (ppr ty)
1144     doInst swapped tv ty (Left cotv) eq
1145       = do { lookupTV <- lookupTcTyVar tv
1146            ; uMeta swapped tv lookupTV ty cotv
1147            }
1148       where
1149         -- meta variable has been filled already
1150         -- => ignore (must be a skolem that was introduced by flattening locals)
1151         uMeta _swapped _tv (IndirectTv _) _ty _cotv
1152           = return Nothing
1153
1154         -- type variable meets type variable
1155         -- => check that tv2 hasn't been updated yet and choose which to update
1156         uMeta swapped tv1 (DoneTv details1) (TyVarTy tv2) cotv
1157           | tv1 == tv2
1158           = panic "TcTyFuns.uMeta: normalisation shouldn't allow x ~ x"
1159
1160           | otherwise
1161           = do { lookupTV2 <- lookupTcTyVar tv2
1162                ; case lookupTV2 of
1163                    IndirectTv ty   ->
1164                      uMeta swapped tv1 (DoneTv details1) ty cotv
1165                    DoneTv details2 ->
1166                      uMetaVar swapped tv1 details1 tv2 details2 cotv
1167                }
1168
1169         ------ Beyond this point we know that ty2 is not a type variable
1170
1171         -- signature skolem meets non-variable type
1172         -- => cannot update (retain the equality)!
1173         uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) _non_tv_ty _cotv
1174           = return $ Just eq
1175
1176         -- updatable meta variable meets non-variable type
1177         -- => occurs check, monotype check, and kinds match check, then update
1178         uMeta swapped tv (DoneTv (MetaTv _ ref)) non_tv_ty cotv
1179           = do {   -- occurs + monotype check
1180                ; mb_ty' <- checkTauTvUpdate tv non_tv_ty
1181
1182                ; case mb_ty' of
1183                    Nothing  ->
1184                      -- normalisation shouldn't leave families in non_tv_ty
1185                      panic "TcTyFuns.uMeta: unexpected synonym family"
1186                    Just ty' ->
1187                      do { checkUpdateMeta swapped tv ref ty'  -- update meta var
1188                         ; writeMetaTyVar cotv ty'             -- update co var
1189                         ; return Nothing
1190                         }
1191                }
1192
1193         uMeta _ _ _ _ _ = panic "TcTyFuns.uMeta"
1194
1195         -- uMetaVar: unify two type variables
1196         -- meta variable meets skolem
1197         -- => just update
1198         uMetaVar swapped tv1 (MetaTv _ ref) tv2 (SkolemTv _) cotv
1199           = do { checkUpdateMeta swapped tv1 ref (mkTyVarTy tv2)
1200                ; writeMetaTyVar cotv (mkTyVarTy tv2)
1201                ; return Nothing
1202                }
1203
1204         -- meta variable meets meta variable
1205         -- => be clever about which of the two to update
1206         --   (from TcUnify.uUnfilledVars minus boxy stuff)
1207         uMetaVar swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) cotv
1208           = do { case (info1, info2) of
1209                    -- Avoid SigTvs if poss
1210                    (SigTv _, _      ) | k1_sub_k2 -> update_tv2
1211                    (_,       SigTv _) | k2_sub_k1 -> update_tv1
1212
1213                    (_,   _) | k1_sub_k2 -> if k2_sub_k1 && nicer_to_update_tv1
1214                                            then update_tv1      -- Same kinds
1215                                            else update_tv2
1216                             | k2_sub_k1 -> update_tv1
1217                             | otherwise -> kind_err
1218               -- Update the variable with least kind info
1219               -- See notes on type inference in Kind.lhs
1220               -- The "nicer to" part only applies if the two kinds are the same,
1221               -- so we can choose which to do.
1222
1223                ; writeMetaTyVar cotv (mkTyVarTy tv2)
1224                ; return Nothing
1225                }
1226           where
1227                 -- Kinds should be guaranteed ok at this point
1228             update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
1229             update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
1230
1231             kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
1232                        unifyKindMisMatch k1 k2
1233
1234             k1 = tyVarKind tv1
1235             k2 = tyVarKind tv2
1236             k1_sub_k2 = k1 `isSubKind` k2
1237             k2_sub_k1 = k2 `isSubKind` k1
1238
1239             nicer_to_update_tv1 = isSystemName (Var.varName tv1)
1240                 -- Try to update sys-y type variables in preference to ones
1241                 -- gotten (say) by instantiating a polymorphic function with
1242                 -- a user-written type sig
1243
1244         uMetaVar _ _ _ _ _ _ = panic "uMetaVar"
1245 \end{code}
1246
1247
1248 %************************************************************************
1249 %*                                                                      *
1250 \section{Errors}
1251 %*                                                                      *
1252 %************************************************************************
1253
1254 The infamous couldn't match expected type soandso against inferred type
1255 somethingdifferent message.
1256
1257 \begin{code}
1258 eqInstMisMatch :: Inst -> TcM a
1259 eqInstMisMatch inst
1260   = ASSERT( isEqInst inst )
1261     setErrCtxt ctxt $ failWithMisMatch ty_act ty_exp
1262   where
1263     (ty_act, ty_exp) = eqInstTys inst
1264     InstLoc _ _ ctxt = instLoc   inst
1265
1266 -----------------------
1267 failWithMisMatch :: TcType -> TcType -> TcM a
1268 -- Generate the message when two types fail to match,
1269 -- going to some trouble to make it helpful.
1270 -- The argument order is: actual type, expected type
1271 failWithMisMatch ty_act ty_exp
1272   = do  { env0 <- tcInitTidyEnv
1273         ; ty_exp <- zonkTcType ty_exp
1274         ; ty_act <- zonkTcType ty_act
1275         ; failWithTcM (misMatchMsg env0 (ty_act, ty_exp))
1276         }
1277
1278 misMatchMsg :: TidyEnv -> (TcType, TcType) -> (TidyEnv, SDoc)
1279 misMatchMsg env0 (ty_act, ty_exp)
1280   = let (env1, pp_exp, extra_exp) = ppr_ty env0 ty_exp
1281         (env2, pp_act, extra_act) = ppr_ty env1 ty_act
1282         msg = sep [sep [ptext (sLit "Couldn't match expected type") <+> pp_exp,
1283                         nest 7 $
1284                               ptext (sLit "against inferred type") <+> pp_act],
1285                    nest 2 (extra_exp $$ extra_act)]
1286     in
1287     (env2, msg)
1288
1289   where
1290     ppr_ty :: TidyEnv -> TcType -> (TidyEnv, SDoc, SDoc)
1291     ppr_ty env ty
1292       = let (env1, tidy_ty) = tidyOpenType env ty
1293             (env2, extra)  = ppr_extra env1 tidy_ty
1294         in
1295         (env2, quotes (ppr tidy_ty), extra)
1296
1297     -- (ppr_extra env ty) shows extra info about 'ty'
1298     ppr_extra :: TidyEnv -> Type -> (TidyEnv, SDoc)
1299     ppr_extra env (TyVarTy tv)
1300       | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv) && not (isUnk tv)
1301       = (env1, pprSkolTvBinding tv1)
1302       where
1303         (env1, tv1) = tidySkolemTyVar env tv
1304
1305     ppr_extra env _ty = (env, empty)            -- Normal case
1306 \end{code}
1307
1308 Warn of loopy local equalities that were dropped.
1309
1310 \begin{code}
1311 warnDroppingLoopyEquality :: TcType -> TcType -> TcM ()
1312 warnDroppingLoopyEquality ty1 ty2
1313   = do { env0 <- tcInitTidyEnv
1314        ; ty1 <- zonkTcType ty1
1315        ; ty2 <- zonkTcType ty2
1316        ; let (env1 , tidy_ty1) = tidyOpenType env0 ty1
1317              (_env2, tidy_ty2) = tidyOpenType env1 ty2
1318        ; addWarnTc $ hang (ptext (sLit "Dropping loopy given equality"))
1319                        2 (quotes (ppr tidy_ty1 <+> text "~" <+> ppr tidy_ty2))
1320        }
1321 \end{code}