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