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