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