compiler/typecheck/TcTyFuns.lhs

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