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   -- normalisation and solving of equalities
  10   EqConfig,
  11   normaliseEqs, propagateEqs, finaliseEqs, normaliseDicts,
  12
  13   -- errors
  14   misMatchMsg, failWithMisMatch,
  15
  16   -- DEPRECATED: interface for the ICFP'08 algorithm
  17   normaliseGivenEqs, normaliseGivenDicts,
  18   normaliseWantedEqs, normaliseWantedDicts,
  19
  20   ) where
  21
  22
  23 #include "HsVersions.h"
  24
  25 --friends
  26 import TcRnMonad
  27 import TcEnv
  28 import Inst
  29 import TcType
  30 import TcMType
  31
  32 -- GHC
  33 import Coercion
  34 import Type
  35 import TypeRep  ( Type(..) )
  36 import TyCon
  37 import HsSyn
  38 import VarEnv
  39 import VarSet
  40 import Var
  41 import Name
  42 import Bag
  43 import Outputable
  44 import SrcLoc   ( Located(..) )
  45 import Maybes
  46 import FastString
  47
  48 -- standard
  49 import Data.List
  50 import Control.Monad
  51 \end{code}
  52
  53
  54 %************************************************************************
  55 %*                                                                      *
  56                 Normalisation of types wrt toplevel equality schemata
  57 %*                                                                      *
  58 %************************************************************************
  59
  60 Unfold a single synonym family instance and yield the witnessing coercion.
  61 Return 'Nothing' if the given type is either not synonym family instance
  62 or is a synonym family instance that has no matching instance declaration.
  63 (Applies only if the type family application is outermost.)
  64
  65 For example, if we have
  66
  67   :Co:R42T a :: T [a] ~ :R42T a
  68
  69 then 'T [Int]' unfolds to (:R42T Int, :Co:R42T Int).
  70
  71 \begin{code}
  72 tcUnfoldSynFamInst :: Type -> TcM (Maybe (Type, Coercion))
  73 tcUnfoldSynFamInst (TyConApp tycon tys)
  74   | not (isOpenSynTyCon tycon)     -- unfold *only* _synonym_ family instances
  75   = return Nothing
  76   | otherwise
  77   = do { -- we only use the indexing arguments for matching,
  78          -- not the additional ones
  79        ; maybeFamInst <- tcLookupFamInst tycon idxTys
  80        ; case maybeFamInst of
  81            Nothing                -> return Nothing
  82            Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc tys',
  83                                                     mkTyConApp coe_tc tys')
  84              where
  85                tys'   = rep_tys ++ restTys
  86                coe_tc = expectJust "TcTyFun.tcUnfoldSynFamInst"
  87                                    (tyConFamilyCoercion_maybe rep_tc)
  88        }
  89     where
  90         n                = tyConArity tycon
  91         (idxTys, restTys) = splitAt n tys
  92 tcUnfoldSynFamInst _other = return Nothing
  93 \end{code}
  94
  95 Normalise 'Type's and 'PredType's by unfolding type family applications where
  96 possible (ie, we treat family instances as a TRS).  Also zonk meta variables.
  97
  98         tcNormaliseFamInst ty = (co, ty')
  99         then   co : ty ~ ty'
 100
 101 \begin{code}
 102 -- |Normalise the given type as far as possible with toplevel equalities.
 103 -- This results in a coercion witnessing the type equality, in addition to the
 104 -- normalised type.
 105 --
 106 tcNormaliseFamInst :: TcType -> TcM (CoercionI, TcType)
 107 tcNormaliseFamInst = tcGenericNormaliseFamInst tcUnfoldSynFamInst
 108
 109 tcNormaliseFamInstPred :: TcPredType -> TcM (CoercionI, TcPredType)
 110 tcNormaliseFamInstPred = tcGenericNormaliseFamInstPred tcUnfoldSynFamInst
 111 \end{code}
 112
 113 %************************************************************************
 114 %*                                                                      *
 115                 Equality Configurations
 116 %*                                                                      *
 117 %************************************************************************
 118
 119 We maintain normalised equalities together with the skolems introduced as
 120 intermediates during flattening of equalities.
 121
 122 !!!TODO: Do we really need to keep track of the skolem variables?  They are at
 123 the moment not used in instantiateAndExtract, but it is hard to say until we
 124 know exactly how finalisation will fianlly look like.
 125
 126 \begin{code}
 127 -- |Configuration of normalised equalities used during solving.
 128 --
 129 data EqConfig = EqConfig { eqs     :: [RewriteInst]
 130                          , skolems :: TyVarSet
 131                          }
 132
 133 addSkolems :: EqConfig -> TyVarSet -> EqConfig
 134 addSkolems eqCfg newSkolems
 135   = eqCfg {skolems = skolems eqCfg `unionVarSet` newSkolems}
 136
 137 addEq :: EqConfig -> RewriteInst -> EqConfig
 138 addEq eqCfg eq = eqCfg {eqs = eq : eqs eqCfg}
 139 \end{code}
 140
 141 The set of operations on an equality configuration.  We obtain the initialise
 142 configuration by normalisation ('normaliseEqs'), solve the equalities by
 143 propagation ('propagateEqs'), and eventually finalise the configuration when
 144 no further propoagation is possible.
 145
 146 !!!TODO: Eventually, normalisation of dictionaries and dictionary
 147 simplification should be included in propagation.
 148
 149 \begin{code}
 150 -- |Turn a set of equalities into an equality configuration for solving.
 151 --
 152 -- Precondition: The Insts are zonked.
 153 --
 154 normaliseEqs :: [Inst] -> TcM EqConfig
 155 normaliseEqs eqs
 156   = do { (eqss, skolemss) <- mapAndUnzipM normEqInst eqs
 157        ; return $ EqConfig { eqs = concat eqss
 158                            , skolems = unionVarSets skolemss
 159                            }
 160        }
 161
 162 -- |Solves the equalities as far as possible by applying propagation rules.
 163 --
 164 propagateEqs :: EqConfig -> TcM EqConfig
 165 propagateEqs eqCfg@(EqConfig {eqs = todoEqs})
 166   = propagate todoEqs (eqCfg {eqs = []})
 167
 168 -- |Finalise a set of equalities after propagation.  The Boolean value is
 169 -- `True' iff any flexible variables, except those introduced by flattening
 170 -- (i.e., those in the `skolems' component of the argument) where instantiated.
 171 -- The returned set of instances are all residual wanteds.
 172 --
 173 finaliseEqs :: EqConfig -> TcM ([Inst], Bool)
 174 finaliseEqs (EqConfig {eqs = eqs, skolems = skolems})
 175   = do { eqs' <- substitute eqs
 176        ; instantiateAndExtract eqs' skolems
 177        }
 178
 179 -- |Normalise a set of class instances under a given equality configuration.
 180 -- Both the class instances and the equality configuration may change.  The
 181 -- function returns 'Nothing' if neither changes.
 182 --
 183 normaliseDicts :: EqConfig -> [Inst] -> TcM (Maybe (EqConfig, [Inst]))
 184 normaliseDicts = error "TcTyFuns.normaliseDicts"
 185 \end{code}
 186
 187
 188 %************************************************************************
 189 %*                                                                      *
 190                 Normalisation of equalities
 191 %*                                                                      *
 192 %************************************************************************
 193
 194 A normal equality is a properly oriented equality with associated coercion
 195 that contains at most one family equality (in its left-hand side) is oriented
 196 such that it may be used as a reqrite rule.  It has one of the following two
 197 forms:
 198
 199 (1) co :: F t1..tn ~ t  (family equalities)
 200 (2) co :: x ~ t         (variable equalities)
 201
 202 Variable equalities fall again in two classes:
 203
 204 (2a) co :: x ~ t, where t is *not* a variable, or
 205 (2b) co :: x ~ y, where x > y.
 206
 207 The types t, t1, ..., tn may not contain any occurrences of synonym
 208 families.  Moreover, in Forms (2) & (3), the left-hand side may not occur in
 209 the right-hand side, and the relation x > y is an arbitrary, but total order
 210 on type variables
 211
 212 !!!TODO: We may need to keep track of swapping for error messages (and to
 213 re-orient on finilisation).
 214
 215 \begin{code}
 216 data RewriteInst
 217   = RewriteVar  -- Form (2) above
 218     { rwi_var   :: TyVar    -- may be rigid or flexible
 219     , rwi_right :: TcType   -- contains no synonym family applications
 220     , rwi_co    :: EqInstCo -- the wanted or given coercion
 221     , rwi_loc   :: InstLoc
 222     , rwi_name  :: Name     -- no semantic significance (cf. TcRnTypes.EqInst)
 223     }
 224   | RewriteFam  -- Forms (1) above
 225     { rwi_fam   :: TyCon    -- synonym family tycon
 226     , rwi_args  :: [Type]   -- contain no synonym family applications
 227     , rwi_right :: TcType   -- contains no synonym family applications
 228     , rwi_co    :: EqInstCo -- the wanted or given coercion
 229     , rwi_loc   :: InstLoc
 230     , rwi_name  :: Name     -- no semantic significance (cf. TcRnTypes.EqInst)
 231     }
 232
 233 isWantedRewriteInst :: RewriteInst -> Bool
 234 isWantedRewriteInst = isWantedCo . rwi_co
 235
 236 rewriteInstToInst :: RewriteInst -> Inst
 237 rewriteInstToInst eq@(RewriteVar {rwi_var = tv})
 238   = EqInst
 239     { tci_left  = mkTyVarTy tv
 240     , tci_right = rwi_right eq
 241     , tci_co    = rwi_co    eq
 242     , tci_loc   = rwi_loc   eq
 243     , tci_name  = rwi_name  eq
 244     }
 245 rewriteInstToInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
 246   = EqInst
 247     { tci_left  = mkTyConApp fam args
 248     , tci_right = rwi_right eq
 249     , tci_co    = rwi_co    eq
 250     , tci_loc   = rwi_loc   eq
 251     , tci_name  = rwi_name  eq
 252     }
 253 \end{code}
 254
 255 The following functions turn an arbitrary equality into a set of normal
 256 equalities.
 257
 258 \begin{code}
 259 normEqInst :: Inst -> TcM ([RewriteInst], TyVarSet)
 260 normEqInst inst
 261   = ASSERT( isEqInst inst )
 262     go ty1 ty2 (eqInstCoercion inst)
 263   where
 264     (ty1, ty2) = eqInstTys inst
 265
 266       -- look through synonyms
 267     go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
 268     go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
 269
 270       -- left-to-right rule with type family head
 271     go (TyConApp con args) ty2 co
 272       | isOpenSynTyCon con
 273       = mkRewriteFam con args ty2 co
 274
 275       -- right-to-left rule with type family head
 276     go ty1 ty2@(TyConApp con args) co
 277       | isOpenSynTyCon con
 278       = do { co' <- mkSymEqInstCo co (ty2, ty1)
 279            ; mkRewriteFam con args ty1 co'
 280            }
 281
 282       -- no outermost family
 283     go ty1 ty2 co
 284       = do { (ty1', co1, ty1_eqs, ty1_skolems) <- flattenType inst ty1
 285            ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2
 286            ; let ty12_eqs  = ty1_eqs ++ ty2_eqs
 287                  rewriteCo = co1 `mkTransCoercion` mkSymCoercion co2
 288                  eqTys     = (ty1', ty2')
 289            ; (co', ty12_eqs') <- adjustCoercions co rewriteCo eqTys ty12_eqs
 290            ; eqs <- checkOrientation ty1' ty2' co' inst
 291            ; return $ (eqs ++ ty12_eqs',
 292                        ty1_skolems `unionVarSet` ty2_skolems)
 293            }
 294
 295     mkRewriteFam con args ty2 co
 296       = do { (args', cargs, args_eqss, args_skolemss)
 297                <- mapAndUnzip4M (flattenType inst) args
 298            ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2
 299            ; let rewriteCo = mkTyConApp con cargs `mkTransCoercion`
 300                              mkSymCoercion co2
 301                  all_eqs   = concat args_eqss ++ ty2_eqs
 302                  eqTys     = (mkTyConApp con args', ty2')
 303            ; (co', all_eqs') <- adjustCoercions co rewriteCo eqTys all_eqs
 304            ; let thisRewriteFam = RewriteFam
 305                                   { rwi_fam   = con
 306                                   , rwi_args  = args'
 307                                   , rwi_right = ty2'
 308                                   , rwi_co    = co'
 309                                   , rwi_loc   = tci_loc inst
 310                                   , rwi_name  = tci_name inst
 311                                   }
 312            ; return $ (thisRewriteFam : all_eqs',
 313                        unionVarSets (ty2_skolems:args_skolemss))
 314            }
 315
 316 checkOrientation :: Type -> Type -> EqInstCo -> Inst -> TcM [RewriteInst]
 317 -- Performs the occurs check, decomposition, and proper orientation
 318 -- (returns a singleton, or an empty list in case of a trivial equality)
 319 -- NB: We cannot assume that the two types already have outermost type
 320 --     synonyms expanded due to the recursion in the case of type applications.
 321 checkOrientation ty1 ty2 co inst
 322   = go ty1 ty2
 323   where
 324       -- look through synonyms
 325     go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
 326     go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
 327
 328       -- identical types => trivial
 329     go ty1 ty2
 330       | ty1 `tcEqType` ty2
 331       = do { mkIdEqInstCo co ty1
 332            ; return []
 333            }
 334
 335       -- two tvs, left greater => unchanged
 336     go ty1@(TyVarTy tv1) ty2@(TyVarTy tv2)
 337       | tv1 > tv2
 338       = mkRewriteVar tv1 ty2 co
 339
 340       -- two tvs, right greater => swap
 341       | otherwise
 342       = do { co' <- mkSymEqInstCo co (ty2, ty1)
 343            ; mkRewriteVar tv2 ty1 co'
 344            }
 345
 346       -- only lhs is a tv => unchanged
 347     go ty1@(TyVarTy tv1) ty2
 348       | ty1 `tcPartOfType` ty2      -- occurs check!
 349       = occurCheckErr ty1 ty2
 350       | otherwise
 351       = mkRewriteVar tv1 ty2 co
 352
 353       -- only rhs is a tv => swap
 354     go ty1 ty2@(TyVarTy tv2)
 355       | ty2 `tcPartOfType` ty1      -- occurs check!
 356       = occurCheckErr ty2 ty1
 357       | otherwise
 358       = do { co' <- mkSymEqInstCo co (ty2, ty1)
 359            ; mkRewriteVar tv2 ty1 co'
 360            }
 361
 362       -- type applications => decompose
 363     go ty1 ty2
 364       | Just (ty1_l, ty1_r) <- repSplitAppTy_maybe ty1   -- won't split fam apps
 365       , Just (ty2_l, ty2_r) <- repSplitAppTy_maybe ty2
 366       = do { (co_l, co_r) <- mkAppEqInstCo co (ty1_l, ty2_l) (ty1_r, ty2_r)
 367            ; eqs_l <- checkOrientation ty1_l ty2_l co_l inst
 368            ; eqs_r <- checkOrientation ty1_r ty2_r co_r inst
 369            ; return $ eqs_l ++ eqs_r
 370            }
 371 -- !!!TODO: would be more efficient to handle the FunApp and the data
 372 -- constructor application explicitly.
 373
 374       -- inconsistency => type error
 375     go ty1 ty2
 376       = ASSERT( (not . isForAllTy $ ty1) && (not . isForAllTy $ ty2) )
 377         eqInstMisMatch inst
 378
 379     mkRewriteVar tv ty co = return [RewriteVar
 380                                     { rwi_var   = tv
 381                                     , rwi_right = ty
 382                                     , rwi_co    = co
 383                                     , rwi_loc   = tci_loc inst
 384                                     , rwi_name  = tci_name inst
 385                                     }]
 386
 387 flattenType :: Inst     -- context to get location  & name
 388             -> Type     -- the type to flatten
 389             -> TcM (Type,           -- the flattened type
 390                     Coercion,       -- coercion witness of flattening wanteds
 391                     [RewriteInst],  -- extra equalities
 392                     TyVarSet)       -- new intermediate skolems
 393 -- Removes all family synonyms from a type by moving them into extra equalities
 394 flattenType inst ty
 395   = go ty
 396   where
 397       -- look through synonyms
 398     go ty | Just ty' <- tcView ty = go ty'
 399
 400       -- type family application => flatten to "id :: F t1'..tn' ~ alpha"
 401     go ty@(TyConApp con args)
 402       | isOpenSynTyCon con
 403       = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args
 404            ; alpha <- newFlexiTyVar (typeKind ty)
 405            ; let alphaTy = mkTyVarTy alpha
 406            ; cotv <- newMetaCoVar (mkTyConApp con args') alphaTy
 407            ; let thisRewriteFam = RewriteFam
 408                                   { rwi_fam   = con
 409                                   , rwi_args  = args'
 410                                   , rwi_right = alphaTy
 411                                   , rwi_co    = mkWantedCo cotv
 412                                   , rwi_loc   = tci_loc inst
 413                                   , rwi_name  = tci_name inst
 414                                   }
 415            ; return (alphaTy,
 416                      mkTyConApp con cargs `mkTransCoercion` mkTyVarTy cotv,
 417                      thisRewriteFam : concat args_eqss,
 418                      unionVarSets args_skolemss `extendVarSet` alpha)
 419            }           -- adding new unflatten var inst
 420
 421       -- data constructor application => flatten subtypes
 422       -- NB: Special cased for efficiency - could be handled as type application
 423     go (TyConApp con args)
 424       = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args
 425            ; return (mkTyConApp con args',
 426                      mkTyConApp con cargs,
 427                      concat args_eqss,
 428                      unionVarSets args_skolemss)
 429            }
 430
 431       -- function type => flatten subtypes
 432       -- NB: Special cased for efficiency - could be handled as type application
 433     go (FunTy ty_l ty_r)
 434       = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l
 435            ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r
 436            ; return (mkFunTy ty_l' ty_r',
 437                      mkFunTy co_l co_r,
 438                      eqs_l ++ eqs_r,
 439                      skolems_l `unionVarSet` skolems_r)
 440            }
 441
 442       -- type application => flatten subtypes
 443     go (AppTy ty_l ty_r)
 444 --      | Just (ty_l, ty_r) <- repSplitAppTy_maybe ty
 445       = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l
 446            ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r
 447            ; return (mkAppTy ty_l' ty_r',
 448                      mkAppTy co_l co_r,
 449                      eqs_l ++ eqs_r,
 450                      skolems_l `unionVarSet` skolems_r)
 451            }
 452
 453       -- free of type families => leave as is
 454     go ty
 455       = ASSERT( not . isForAllTy $ ty )
 456         return (ty, ty, [] , emptyVarSet)
 457
 458 adjustCoercions :: EqInstCo            -- coercion of original equality
 459                 -> Coercion            -- coercion witnessing the rewrite
 460                 -> (Type, Type)        -- type sof flattened equality
 461                 -> [RewriteInst]       -- equalities from flattening
 462                 -> TcM (EqInstCo,      -- coercion for flattened equality
 463                         [RewriteInst]) -- final equalities from flattening
 464 -- Depending on whether we flattened a local or wanted equality, that equality's
 465 -- coercion and that of the new ones are adjusted
 466 adjustCoercions co rewriteCo eqTys all_eqs
 467   | isWantedCo co
 468   = do { co' <- mkRightTransEqInstCo co rewriteCo eqTys
 469        ; return (co', all_eqs)
 470        }
 471   | otherwise
 472   = return (co, map wantedToLocal all_eqs)
 473   where
 474     wantedToLocal eq = eq {rwi_co = mkGivenCo (rwi_right eq)}
 475 \end{code}
 476
 477
 478 %************************************************************************
 479 %*                                                                      *
 480                 Propagation of equalities
 481 %*                                                                      *
 482 %************************************************************************
 483
 484 Apply the propagation rules exhaustively.
 485
 486 \begin{code}
 487 propagate :: [RewriteInst] -> EqConfig -> TcM EqConfig
 488 propagate []       eqCfg = return eqCfg
 489 propagate (eq:eqs) eqCfg
 490   = do { optEqs <- applyTop eq
 491        ; case optEqs of
 492
 493               -- Top applied to 'eq' => retry with new equalities
 494            Just (eqs2, skolems2)
 495              -> propagate (eqs2 ++ eqs) (eqCfg `addSkolems` skolems2)
 496
 497               -- Top doesn't apply => try subst rules with all other
 498               --   equalities, after that 'eq' can go into the residual list
 499            Nothing
 500              -> do { (eqs', eqCfg') <- applySubstRules eq eqs eqCfg
 501                    ; propagate eqs' (eqCfg' `addEq` eq)
 502                    }
 503    }
 504
 505 applySubstRules :: RewriteInst                    -- currently considered eq
 506                 -> [RewriteInst]                  -- todo eqs list
 507                 -> EqConfig                       -- residual
 508                 -> TcM ([RewriteInst], EqConfig)  -- new todo & residual
 509 applySubstRules eq todoEqs (eqConfig@EqConfig {eqs = resEqs})
 510   = do { (newEqs_t, unchangedEqs_t, skolems_t) <- mapSubstRules eq todoEqs
 511        ; (newEqs_r, unchangedEqs_r, skolems_r) <- mapSubstRules eq resEqs
 512        ; return (newEqs_t ++ newEqs_r ++ unchangedEqs_t,
 513                  eqConfig {eqs = unchangedEqs_r}
 514                    `addSkolems` (skolems_t `unionVarSet` skolems_r))
 515        }
 516
 517 mapSubstRules :: RewriteInst     -- try substituting this equality
 518               -> [RewriteInst]   -- into these equalities
 519               -> TcM ([RewriteInst], [RewriteInst], TyVarSet)
 520 mapSubstRules eq eqs
 521   = do { (newEqss, unchangedEqss, skolemss) <- mapAndUnzip3M (substRules eq) eqs
 522        ; return (concat newEqss, concat unchangedEqss, unionVarSets skolemss)
 523        }
 524   where
 525     substRules eq1 eq2
 526       = do {   -- try the SubstFam rule
 527              optEqs <- applySubstFam eq1 eq2
 528            ; case optEqs of
 529                Just (eqs, skolems) -> return (eqs, [], skolems)
 530                Nothing             -> do
 531            {   -- try the SubstVarVar rule
 532              optEqs <- applySubstVarVar eq1 eq2
 533            ; case optEqs of
 534                Just (eqs, skolems) -> return (eqs, [], skolems)
 535                Nothing             -> do
 536            {   -- try the SubstVarFam rule
 537              optEqs <- applySubstVarFam eq1 eq2
 538            ; case optEqs of
 539                Just eq -> return ([eq], [], emptyVarSet)
 540                Nothing -> return ([], [eq2], emptyVarSet)
 541                  -- if no rule matches, we return the equlity we tried to
 542                  -- substitute into unchanged
 543            }}}
 544 \end{code}
 545
 546 Attempt to apply the Top rule.  The rule is
 547
 548   co :: F t1..tn ~ t
 549   =(Top)=>
 550   co' :: [s1/x1, .., sm/xm]s ~ t with co = g s1..sm |> co'
 551
 552 where g :: forall x1..xm. F u1..um ~ s and [s1/x1, .., sm/xm]u1 == t1.
 553
 554 Returns Nothing if the rule could not be applied.  Otherwise, the resulting
 555 equality is normalised and a list of the normal equalities is returned.
 556
 557 \begin{code}
 558 applyTop :: RewriteInst -> TcM (Maybe ([RewriteInst], TyVarSet))
 559
 560 applyTop eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
 561   = do { optTyCo <- tcUnfoldSynFamInst (TyConApp fam args)
 562        ; case optTyCo of
 563            Nothing                -> return Nothing
 564            Just (lhs, rewrite_co)
 565              -> do { co' <- mkRightTransEqInstCo co rewrite_co (lhs, rhs)
 566                    ; let eq' = EqInst
 567                                { tci_left  = lhs
 568                                , tci_right = rhs
 569                                , tci_co    = co'
 570                                , tci_loc   = rwi_loc eq
 571                                , tci_name  = rwi_name eq
 572                                }
 573                    ; liftM Just $ normEqInst eq'
 574                    }
 575        }
 576   where
 577     co  = rwi_co eq
 578     rhs = rwi_right eq
 579
 580 applyTop _ = return Nothing
 581 \end{code}
 582
 583 Attempt to apply the SubstFam rule.  The rule is
 584
 585   co1 :: F t1..tn ~ t  &  co2 :: F t1..tn ~ s
 586   =(SubstFam)=>
 587   co1 :: F t1..tn ~ t  &  co2' :: t ~ s with co2 = co1 |> co2'
 588
 589 where co1 may be a wanted only if co2 is a wanted, too.
 590
 591 Returns Nothing if the rule could not be applied.  Otherwise, the equality
 592 co2' is normalised and a list of the normal equalities is returned.  (The
 593 equality co1 is not returned as it remain unaltered.)
 594
 595 \begin{code}
 596 applySubstFam :: RewriteInst
 597               -> RewriteInst
 598               -> TcM (Maybe ([RewriteInst], TyVarSet))
 599 applySubstFam eq1@(RewriteFam {rwi_fam = fam1, rwi_args = args1})
 600               eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
 601   | fam1 == fam2 && tcEqTypes args1 args2 &&
 602     (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
 603 -- !!!TODO: tcEqTypes is insufficient as it does not look through type synonyms
 604 -- !!!Check whether anything breaks by making tcEqTypes look through synonyms.
 605 -- !!!Should be ok and we don't want three type equalities.
 606   = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
 607        ; let eq2' = EqInst
 608                     { tci_left  = lhs
 609                     , tci_right = rhs
 610                     , tci_co    = co2'
 611                     , tci_loc   = rwi_loc eq2
 612                     , tci_name  = rwi_name eq2
 613                     }
 614        ; liftM Just $ normEqInst eq2'
 615        }
 616   where
 617     lhs = rwi_right eq1
 618     rhs = rwi_right eq2
 619     co1 = eqInstCoType (rwi_co eq1)
 620     co2 = rwi_co eq2
 621 applySubstFam _ _ = return Nothing
 622 \end{code}
 623
 624 Attempt to apply the SubstVarVar rule.  The rule is
 625
 626   co1 :: x ~ t  &  co2 :: x ~ s
 627   =(SubstVarVar)=>
 628   co1 :: x ~ t  &  co2' :: t ~ s with co2 = co1 |> co2'
 629
 630 where co1 may be a wanted only if co2 is a wanted, too.
 631
 632 Returns Nothing if the rule could not be applied.  Otherwise, the equality
 633 co2' is normalised and a list of the normal equalities is returned.  (The
 634 equality co1 is not returned as it remain unaltered.)
 635
 636 \begin{code}
 637 applySubstVarVar :: RewriteInst
 638                  -> RewriteInst
 639                  -> TcM (Maybe ([RewriteInst], TyVarSet))
 640 applySubstVarVar eq1@(RewriteVar {rwi_var = tv1})
 641                  eq2@(RewriteVar {rwi_var = tv2})
 642   | tv1 == tv2 &&
 643     (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
 644   = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
 645        ; let eq2' = EqInst
 646                     { tci_left  = lhs
 647                     , tci_right = rhs
 648                     , tci_co    = co2'
 649                     , tci_loc   = rwi_loc eq2
 650                     , tci_name  = rwi_name eq2
 651                     }
 652        ; liftM Just $ normEqInst eq2'
 653        }
 654   where
 655     lhs = rwi_right eq1
 656     rhs = rwi_right eq2
 657     co1 = eqInstCoType (rwi_co eq1)
 658     co2 = rwi_co eq2
 659 applySubstVarVar _ _ = return Nothing
 660 \end{code}
 661
 662 Attempt to apply the SubstVarFam rule.  The rule is
 663
 664   co1 :: x ~ t  &  co2 :: F s1..sn ~ s
 665   =(SubstVarFam)=>
 666   co1 :: x ~ t  &  co2' :: [t/x](F s1..sn) ~ s
 667     with co2 = [co1/x](F s1..sn) |> co2'
 668
 669 where x occurs in F s1..sn. (co1 may be local or wanted.)
 670
 671 Returns Nothing if the rule could not be applied.  Otherwise, the equality
 672 co2' is returned.  (The equality co1 is not returned as it remain unaltered.)
 673
 674 \begin{code}
 675 applySubstVarFam :: RewriteInst -> RewriteInst -> TcM (Maybe RewriteInst)
 676 applySubstVarFam eq1@(RewriteVar {rwi_var = tv1})
 677                  eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
 678   | tv1 `elemVarSet` tyVarsOfTypes args2
 679   = do { let co1Subst = substTyWith [tv1] [co1] (mkTyConApp fam2 args2)
 680              args2'   = substTysWith [tv1] [rhs1] args2
 681              lhs2     = mkTyConApp fam2 args2'
 682        ; co2' <- mkRightTransEqInstCo co2 co1Subst (lhs2, rhs2)
 683        ; return $ Just (eq2 {rwi_args = args2', rwi_co = co2'})
 684        }
 685   where
 686     rhs1 = rwi_right eq1
 687     rhs2 = rwi_right eq2
 688     co1  = eqInstCoType (rwi_co eq1)
 689     co2  = rwi_co eq2
 690 applySubstVarFam _ _ = return Nothing
 691 \end{code}
 692
 693
 694 %************************************************************************
 695 %*                                                                      *
 696                 Finalisation of equalities
 697 %*                                                                      *
 698 %************************************************************************
 699
 700 Exhaustive substitution of all variable equalities of the form co :: x ~ t
 701 (both local and wanted) into the left-hand sides all other equalities.  This
 702 may lead to recursive equalities; i.e., (1) we need to apply the substitution
 703 implied by one variable equality exhaustively before turning to the next and
 704 (2) we need an occurs check.
 705
 706 NB: Gievn that we apply the substitution corresponding to a single equality
 707 exhaustively, before turning to the next, and because we eliminate recursive
 708 eqaulities, all opportunities for subtitution will have been exhausted after
 709 we have considered each equality once.
 710
 711 \begin{code}
 712 substitute :: [RewriteInst] -> TcM [RewriteInst]
 713 substitute eqs = subst eqs []
 714   where
 715     subst []       res = return res
 716     subst (eq:eqs) res
 717       = do { eqs' <- mapM (substOne eq) eqs
 718            ; res' <- mapM (substOne eq) res
 719            ; subst eqs' (eq:res')
 720            }
 721
 722       -- apply [ty/tv] to left-hand side of eq2
 723     substOne (RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}) eq2
 724       = do { let co1Subst = mkSymCoercion $
 725                               substTyWith [tv] [eqInstCoType co] (rwi_right eq2)
 726                  right2'  = substTyWith [tv] [ty] (rwi_right eq2)
 727                  left2    = case eq2 of
 728                               RewriteVar {rwi_var = tv2}   -> mkTyVarTy tv2
 729                               RewriteFam {rwi_fam = fam,
 730                                           rwi_args = args} ->mkTyConApp fam args
 731            ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2')
 732            ; case eq2 of
 733                RewriteVar {rwi_var = tv2} | tv2 `elemVarSet` tyVarsOfType ty
 734                  -> occurCheckErr left2 right2'
 735                _ -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
 736            }
 737
 738       -- changed
 739     substOne _ eq2
 740       = return eq2
 741 \end{code}
 742
 743 For any *wanted* variable equality of the form co :: alpha ~ t or co :: a ~
 744 alpha, we instantiate alpha with t or a, respectively, and set co := id.
 745 Return all remaining wanted equalities.  The Boolean result component is True
 746 if at least one instantiation of a flexible was performed.
 747
 748 \begin{code}
 749 instantiateAndExtract :: [RewriteInst] -> TyVarSet -> TcM ([Inst], Bool)
 750 instantiateAndExtract eqs _skolems
 751   = do { let wanteds = filter (isWantedCo . rwi_co) eqs
 752        ; wanteds' <- mapM inst wanteds
 753        ; let residuals = catMaybes wanteds'
 754              improved  = length wanteds /= length residuals
 755        ; return (map rewriteInstToInst residuals, improved)
 756        }
 757   where
 758     inst eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co})
 759
 760         -- co :: alpha ~ t
 761       | isMetaTyVar tv1
 762       = doInst tv1 ty2 co eq
 763
 764         -- co :: a ~ alpha
 765       | Just tv2 <- tcGetTyVar_maybe ty2
 766       , isMetaTyVar tv2
 767       = doInst tv2 (mkTyVarTy tv1) co eq
 768
 769     inst eq = return $ Just eq
 770
 771     doInst _  _  (Right ty)  _eq = pprPanic "TcTyFuns.doInst: local eq: "
 772                                            (ppr ty)
 773     doInst tv ty (Left cotv) eq  = do { lookupTV <- lookupTcTyVar tv
 774                                       ; uMeta False tv lookupTV ty cotv
 775                                       }
 776       where
 777         -- meta variable has been filled already
 778         -- => panic (all equalities should have been zonked on normalisation)
 779         uMeta _swapped _tv (IndirectTv _) _ty _cotv
 780           = panic "TcTyFuns.uMeta: expected zonked equalities"
 781
 782         -- type variable meets type variable
 783         -- => check that tv2 hasn't been updated yet and choose which to update
 784         uMeta swapped tv1 (DoneTv details1) (TyVarTy tv2) cotv
 785           | tv1 == tv2
 786           = panic "TcTyFuns.uMeta: normalisation shouldn't allow x ~ x"
 787
 788           | otherwise
 789           = do { lookupTV2 <- lookupTcTyVar tv2
 790                ; case lookupTV2 of
 791                    IndirectTv ty   ->
 792                      uMeta swapped tv1 (DoneTv details1) ty cotv
 793                    DoneTv details2 ->
 794                      uMetaVar swapped tv1 details1 tv2 details2 cotv
 795                }
 796
 797         ------ Beyond this point we know that ty2 is not a type variable
 798
 799         -- signature skolem meets non-variable type
 800         -- => cannot update (retain the equality)!
 801         uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) _non_tv_ty _cotv
 802           = return $ Just eq
 803
 804         -- updatable meta variable meets non-variable type
 805         -- => occurs check, monotype check, and kinds match check, then update
 806         uMeta swapped tv (DoneTv (MetaTv _ ref)) non_tv_ty cotv
 807           = do {   -- occurs + monotype check
 808                ; mb_ty' <- checkTauTvUpdate tv non_tv_ty
 809
 810                ; case mb_ty' of
 811                    Nothing  ->
 812                      -- normalisation shouldn't leave families in non_tv_ty
 813                      panic "TcTyFuns.uMeta: unexpected synonym family"
 814                    Just ty' ->
 815                      do { checkUpdateMeta swapped tv ref ty'  -- update meta var
 816                         ; writeMetaTyVar cotv ty'             -- update co var
 817                         ; return Nothing
 818                         }
 819                }
 820
 821         uMeta _ _ _ _ _ = panic "TcTyFuns.uMeta"
 822
 823         -- uMetaVar: unify two type variables
 824         -- meta variable meets skolem
 825         -- => just update
 826         uMetaVar swapped tv1 (MetaTv _ ref) tv2 (SkolemTv _) cotv
 827           = do { checkUpdateMeta swapped tv1 ref (mkTyVarTy tv2)
 828                ; writeMetaTyVar cotv (mkTyVarTy tv2)
 829                ; return Nothing
 830                }
 831
 832         -- meta variable meets meta variable
 833         -- => be clever about which of the two to update
 834         --   (from TcUnify.uUnfilledVars minus boxy stuff)
 835         uMetaVar swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) cotv
 836           = do { case (info1, info2) of
 837                    -- Avoid SigTvs if poss
 838                    (SigTv _, _      ) | k1_sub_k2 -> update_tv2
 839                    (_,       SigTv _) | k2_sub_k1 -> update_tv1
 840
 841                    (_,   _) | k1_sub_k2 -> if k2_sub_k1 && nicer_to_update_tv1
 842                                            then update_tv1      -- Same kinds
 843                                            else update_tv2
 844                             | k2_sub_k1 -> update_tv1
 845                             | otherwise -> kind_err
 846               -- Update the variable with least kind info
 847               -- See notes on type inference in Kind.lhs
 848               -- The "nicer to" part only applies if the two kinds are the same,
 849               -- so we can choose which to do.
 850
 851                ; writeMetaTyVar cotv (mkTyVarTy tv2)
 852                ; return Nothing
 853                }
 854           where
 855                 -- Kinds should be guaranteed ok at this point
 856             update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
 857             update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
 858
 859             kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
 860                        unifyKindMisMatch k1 k2
 861
 862             k1 = tyVarKind tv1
 863             k2 = tyVarKind tv2
 864             k1_sub_k2 = k1 `isSubKind` k2
 865             k2_sub_k1 = k2 `isSubKind` k1
 866
 867             nicer_to_update_tv1 = isSystemName (Var.varName tv1)
 868                 -- Try to update sys-y type variables in preference to ones
 869                 -- gotten (say) by instantiating a polymorphic function with
 870                 -- a user-written type sig
 871
 872         uMetaVar _ _ _ _ _ _ = panic "uMetaVar"
 873 \end{code}
 874
 875
 876
 877 ==================== CODE FOR THE OLD ICFP'08 ALGORITHM ======================
 878
 879 An elementary rewrite is a properly oriented equality with associated coercion
 880 that has one of the following two forms:
 881
 882 (1) co :: F t1..tn ~ t
 883 (2) co :: a ~ t         , where t /= F t1..tn and a is a skolem tyvar
 884
 885 NB: We do *not* use equalities of the form a ~ t where a is a meta tyvar as a
 886 reqrite rule.  Instead, such equalities are solved by unification.  This is
 887 essential; cf Note [skolemOccurs loop].
 888
 889 The following functions takes an equality instance and turns it into an
 890 elementary rewrite if possible.
 891
 892 \begin{code}
 893 data Rewrite = Rewrite TcType           -- lhs of rewrite rule
 894                        TcType           -- rhs of rewrite rule
 895                        TcType           -- coercion witnessing the rewrite rule
 896
 897 eqInstToRewrite :: Inst -> Maybe (Rewrite, Bool)
 898                                            -- True iff rewrite swapped equality
 899 eqInstToRewrite inst
 900   = ASSERT( isEqInst inst )
 901     go ty1 ty2 (eqInstType inst)
 902   where
 903     (ty1,ty2) = eqInstTys inst
 904
 905     -- look through synonyms
 906     go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
 907     go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
 908
 909     -- left-to-right rule with type family head
 910     go ty1@(TyConApp con _) ty2 co
 911       | isOpenSynTyCon con
 912       = Just (Rewrite ty1 ty2 co, False)                     -- not swapped
 913
 914     -- left-to-right rule with type variable head
 915     go ty1@(TyVarTy tv) ty2 co
 916       | isSkolemTyVar tv
 917       = Just (Rewrite ty1 ty2 co, False)                     -- not swapped
 918
 919     -- right-to-left rule with type family head, only after
 920     -- having checked whether we can work left-to-right
 921     go ty1 ty2@(TyConApp con _) co
 922       | isOpenSynTyCon con
 923       = Just (Rewrite ty2 ty1 (mkSymCoercion co), True)      -- swapped
 924
 925     -- right-to-left rule with type variable head, only after
 926     -- having checked whether we can work left-to-right
 927     go ty1 ty2@(TyVarTy tv) co
 928       | isSkolemTyVar tv
 929       = Just (Rewrite ty2 ty1 (mkSymCoercion co), True)      -- swapped
 930
 931     -- this equality is not a rewrite rule => ignore
 932     go _ _ _ = Nothing
 933 \end{code}
 934
 935 Normalise a type relative to an elementary rewrite implied by an EqInst or an
 936 explicitly given elementary rewrite.
 937
 938 \begin{code}
 939 -- Rewrite by EqInst
 940 --   Precondition: the EqInst passes the occurs check
 941 tcEqInstNormaliseFamInst :: Inst -> TcType -> TcM (CoercionI, TcType)
 942 tcEqInstNormaliseFamInst inst ty
 943   = case eqInstToRewrite inst of
 944       Just (rewrite, _) -> tcEqRuleNormaliseFamInst rewrite ty
 945       Nothing           -> return (IdCo, ty)
 946
 947 -- Rewrite by equality rewrite rule
 948 tcEqRuleNormaliseFamInst :: Rewrite                     -- elementary rewrite
 949                          -> TcType                      -- type to rewrite
 950                          -> TcM (CoercionI,             -- witnessing coercion
 951                                  TcType)                -- rewritten type
 952 tcEqRuleNormaliseFamInst (Rewrite pat rhs co) ty
 953   = tcGenericNormaliseFamInst matchEqRule ty
 954   where
 955     matchEqRule sty | pat `tcEqType` sty = return $ Just (rhs, co)
 956                     | otherwise          = return $ Nothing
 957 \end{code}
 958
 959 Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
 960 apply the normalisation function gives as the first argument to every TyConApp
 961 and every TyVarTy subterm.
 962
 963         tcGenericNormaliseFamInst fun ty = (co, ty')
 964         then   co : ty ~ ty'
 965
 966 This function is (by way of using smart constructors) careful to ensure that
 967 the returned coercion is exactly IdCo (and not some semantically equivalent,
 968 but syntactically different coercion) whenever (ty' `tcEqType` ty).  This
 969 makes it easy for the caller to determine whether the type changed.  BUT
 970 even if we return IdCo, ty' may be *syntactically* different from ty due to
 971 unfolded closed type synonyms (by way of tcCoreView).  In the interest of
 972 good error messages, callers should discard ty' in favour of ty in this case.
 973
 974 \begin{code}
 975 tcGenericNormaliseFamInst :: (TcType -> TcM (Maybe (TcType, Coercion)))
 976                              -- what to do with type functions and tyvars
 977                            -> TcType                    -- old type
 978                            -> TcM (CoercionI, TcType)   -- (coercion, new type)
 979 tcGenericNormaliseFamInst fun ty
 980   | Just ty' <- tcView ty = tcGenericNormaliseFamInst fun ty'
 981 tcGenericNormaliseFamInst fun (TyConApp tyCon tys)
 982   = do  { (cois, ntys) <- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
 983         ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
 984         ; maybe_ty_co <- fun (mkTyConApp tyCon ntys)     -- use normalised args!
 985         ; case maybe_ty_co of
 986             -- a matching family instance exists
 987             Just (ty', co) ->
 988               do { let first_coi = mkTransCoI tycon_coi (ACo co)
 989                  ; (rest_coi, nty) <- tcGenericNormaliseFamInst fun ty'
 990                  ; let fix_coi = mkTransCoI first_coi rest_coi
 991                  ; return (fix_coi, nty)
 992                  }
 993             -- no matching family instance exists
 994             -- we do not do anything
 995             Nothing -> return (tycon_coi, mkTyConApp tyCon ntys)
 996         }
 997 tcGenericNormaliseFamInst fun (AppTy ty1 ty2)
 998   = do  { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
 999         ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
1000         ; return (mkAppTyCoI nty1 coi1 nty2 coi2, mkAppTy nty1 nty2)
1001         }
1002 tcGenericNormaliseFamInst fun (FunTy ty1 ty2)
1003   = do  { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
1004         ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
1005         ; return (mkFunTyCoI nty1 coi1 nty2 coi2, mkFunTy nty1 nty2)
1006         }
1007 tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1)
1008   = do  { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
1009         ; return (mkForAllTyCoI tyvar coi, mkForAllTy tyvar nty1)
1010         }
1011 tcGenericNormaliseFamInst fun ty@(TyVarTy tv)
1012   | isTcTyVar tv
1013   = do  { traceTc (text "tcGenericNormaliseFamInst" <+> ppr ty)
1014         ; res <- lookupTcTyVar tv
1015         ; case res of
1016             DoneTv _ ->
1017               do { maybe_ty' <- fun ty
1018                  ; case maybe_ty' of
1019                      Nothing         -> return (IdCo, ty)
1020                      Just (ty', co1) ->
1021                        do { (coi2, ty'') <- tcGenericNormaliseFamInst fun ty'
1022                           ; return (ACo co1 `mkTransCoI` coi2, ty'')
1023                           }
1024                  }
1025             IndirectTv ty' -> tcGenericNormaliseFamInst fun ty'
1026         }
1027   | otherwise
1028   = return (IdCo, ty)
1029 tcGenericNormaliseFamInst fun (PredTy predty)
1030   = do  { (coi, pred') <- tcGenericNormaliseFamInstPred fun predty
1031         ; return (coi, PredTy pred') }
1032
1033 ---------------------------------
1034 tcGenericNormaliseFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
1035                               -> TcPredType
1036                               -> TcM (CoercionI, TcPredType)
1037
1038 tcGenericNormaliseFamInstPred fun (ClassP cls tys)
1039   = do { (cois, tys')<- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
1040        ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
1041        }
1042 tcGenericNormaliseFamInstPred fun (IParam ipn ty)
1043   = do { (coi, ty') <- tcGenericNormaliseFamInst fun ty
1044        ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
1045        }
1046 tcGenericNormaliseFamInstPred fun (EqPred ty1 ty2)
1047   = do { (coi1, ty1') <- tcGenericNormaliseFamInst fun ty1
1048        ; (coi2, ty2') <- tcGenericNormaliseFamInst fun ty2
1049        ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
1050 \end{code}
1051
1052
1053 %************************************************************************
1054 %*                                                                      *
1055 \section{Normalisation of equality constraints}
1056 %*                                                                      *
1057 %************************************************************************
1058
1059 Note [Inconsistencies in equality constraints]
1060 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1061 We guarantee that we raise an error if we discover any inconsistencies (i.e.,
1062 equalities that if presented to the unifer in TcUnify would result in an
1063 error) during normalisation of wanted constraints.  This is especially so that
1064 we don't solve wanted constraints under an inconsistent given set.  In
1065 particular, we don't want to permit signatures, such as
1066
1067   bad :: (Int ~ Bool => Int) -> a -> a
1068
1069 \begin{code}
1070 normaliseGivenEqs :: [Inst] -> TcM ([Inst], TcM ())
1071 normaliseGivenEqs givens
1072  = do { traceTc (text "normaliseGivenEqs <-" <+> ppr givens)
1073       ; (result, deSkolem) <-
1074           rewriteToFixedPoint (Just ("(SkolemOccurs)", skolemOccurs))
1075             [ ("(ZONK)",    dontRerun $ zonkInsts)
1076             , ("(TRIVIAL)", dontRerun $ trivialRule)
1077             , ("(DECOMP)",  decompRule)
1078             , ("(TOP)",     topRule)
1079             , ("(SUBST)",   substRule)                   -- incl. occurs check
1080             ] givens
1081       ; traceTc (text "normaliseGivenEqs ->" <+> ppr result)
1082       ; return (result, deSkolem)
1083       }
1084 \end{code}
1085
1086 \begin{code}
1087 normaliseWantedEqs :: [Inst]        -- givens
1088                    -> [Inst]        -- wanteds
1089                    -> TcM [Inst]    -- irreducible wanteds
1090 normaliseWantedEqs givens wanteds
1091   = do { traceTc $ text "normaliseWantedEqs <-" <+> ppr wanteds
1092                    <+> text "with" <+> ppr givens
1093        ; result <- liftM fst $ rewriteToFixedPoint Nothing
1094                      [ ("(ZONK)",    dontRerun $ zonkInsts)
1095                      , ("(TRIVIAL)", dontRerun $ trivialRule)
1096                      , ("(DECOMP)",  decompRule)
1097                      , ("(TOP)",     topRule)
1098                      , ("(GIVEN)",   substGivens givens) -- incl. occurs check
1099                      , ("(UNIFY)",   unifyMetaRule)      -- incl. occurs check
1100                      , ("(SUBST)",   substRule)          -- incl. occurs check
1101                      ] wanteds
1102        ; traceTc (text "normaliseWantedEqs ->" <+> ppr result)
1103        ; return result
1104        }
1105   where
1106     -- Use `substInst' with every given on all the wanteds.
1107     substGivens :: [Inst] -> [Inst] -> TcM ([Inst], Bool)
1108     substGivens []     wanteds = return (wanteds, False)
1109     substGivens (g:gs) wanteds
1110       = do { (wanteds1, changed1) <- substGivens gs wanteds
1111            ; (wanteds2, changed2) <- substInst g wanteds1
1112            ; return (wanteds2, changed1 || changed2)
1113            }
1114 \end{code}
1115
1116
1117 %************************************************************************
1118 %*                                                                      *
1119 \section{Normalisation of non-equality dictionaries}
1120 %*                                                                      *
1121 %************************************************************************
1122
1123 \begin{code}
1124 normaliseGivenDicts, normaliseWantedDicts
1125         :: [Inst]               -- given equations
1126         -> [Inst]               -- dictionaries
1127         -> TcM ([Inst],TcDictBinds)
1128
1129 normaliseGivenDicts  eqs dicts = normalise_dicts eqs dicts False
1130 normaliseWantedDicts eqs dicts = normalise_dicts eqs dicts True
1131
1132 normalise_dicts
1133         :: [Inst]       -- given equations
1134         -> [Inst]       -- dictionaries
1135         -> Bool         -- True <=> the dicts are wanted
1136                         -- Fals <=> they are given
1137         -> TcM ([Inst],TcDictBinds)
1138 normalise_dicts given_eqs dicts is_wanted
1139   = do  { traceTc $ let name | is_wanted = "normaliseWantedDicts <-"
1140                              | otherwise = "normaliseGivenDicts <-"
1141                     in
1142                     text name <+> ppr dicts <+>
1143                     text "with" <+> ppr given_eqs
1144         ; (dicts0, binds0)  <- normaliseInsts is_wanted dicts
1145         ; (dicts1, binds1)  <- substEqInDictInsts is_wanted given_eqs dicts0
1146         ; let binds01 = binds0 `unionBags` binds1
1147         ; if isEmptyBag binds1
1148           then return (dicts1, binds01)
1149           else do { (dicts2, binds2) <-
1150                       normalise_dicts given_eqs dicts1 is_wanted
1151                   ; return (dicts2, binds01 `unionBags` binds2) } }
1152 \end{code}
1153
1154
1155 %************************************************************************
1156 %*                                                                      *
1157 \section{Normalisation rules and iterative rule application}
1158 %*                                                                      *
1159 %************************************************************************
1160
1161 We have three kinds of normalising rewrite rules:
1162
1163 (1) Normalisation rules that rewrite a set of insts and return a flag indicating
1164     whether any changes occurred during rewriting that necessitate re-running
1165     the current rule set.
1166
1167 (2) Precondition rules that rewrite a set of insts and return a monadic action
1168     that reverts the effect of preconditioning.
1169
1170 (3) Idempotent normalisation rules that never require re-running the rule set.
1171
1172 \begin{code}
1173 type RewriteRule     = [Inst] -> TcM ([Inst], Bool)   -- rewrite, maybe re-run
1174 type PrecondRule     = [Inst] -> TcM ([Inst], TcM ()) -- rewrite, revertable
1175 type IdemRewriteRule = [Inst] -> TcM [Inst]           -- rewrite, don't re-run
1176
1177 type NamedRule       = (String, RewriteRule)          -- rule with description
1178 type NamedPreRule    = (String, PrecondRule)          -- precond with desc
1179 \end{code}
1180
1181 Template lifting idempotent rules to full rules (which can be put into a rule
1182 set).
1183
1184 \begin{code}
1185 dontRerun :: IdemRewriteRule -> RewriteRule
1186 dontRerun rule insts = liftM addFalse $ rule insts
1187   where
1188     addFalse x = (x, False)
1189 \end{code}
1190
1191 The following function applies a set of rewrite rules until a fixed point is
1192 reached; i.e., none of the `RewriteRule's require re-running the rule set.
1193 Optionally, there may be a pre-conditing rule that is applied before any other
1194 rules are applied and before the rule set is re-run.
1195
1196 The result is the set of rewritten (i.e., normalised) insts and, in case of a
1197 pre-conditing rule, a monadic action that reverts the effects of
1198 pre-conditioning - specifically, this is removing introduced skolems.
1199
1200 \begin{code}
1201 rewriteToFixedPoint :: Maybe NamedPreRule   -- optional preconditioning rule
1202                     -> [NamedRule]          -- rule set
1203                     -> [Inst]               -- insts to rewrite
1204                     -> TcM ([Inst], TcM ())
1205 rewriteToFixedPoint precondRule rules insts
1206   = completeRewrite (return ()) precondRule insts
1207   where
1208     completeRewrite :: TcM () -> Maybe NamedPreRule -> [Inst]
1209                     -> TcM ([Inst], TcM ())
1210     completeRewrite dePrecond (Just (precondName, precond)) insts
1211       = do { traceTc $ text precondName <+> text " <- " <+> ppr insts
1212            ; (insts', dePrecond') <- precond insts
1213            ; traceTc $ text precondName <+> text " -> " <+> ppr insts'
1214            ; tryRules (dePrecond >> dePrecond') rules insts'
1215            }
1216     completeRewrite dePrecond Nothing insts
1217       = tryRules dePrecond rules insts
1218
1219     tryRules dePrecond _                    []    = return ([]   , dePrecond)
1220     tryRules dePrecond []                   insts = return (insts, dePrecond)
1221     tryRules dePrecond ((name, rule):rules) insts
1222       = do { traceTc $ text name <+> text " <- " <+> ppr insts
1223            ; (insts', rerun) <- rule insts
1224            ; traceTc $ text name <+> text " -> " <+> ppr insts'
1225            ; if rerun then completeRewrite dePrecond precondRule insts'
1226                       else tryRules dePrecond rules insts'
1227            }
1228 \end{code}
1229
1230
1231 %************************************************************************
1232 %*                                                                      *
1233 \section{Different forms of Inst rewrite rules}
1234 %*                                                                      *
1235 %************************************************************************
1236
1237 Splitting of non-terminating given constraints: skolemOccurs
1238 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1239 This is a preconditioning rule exclusively applied to given constraints.
1240 Moreover, its rewriting is only temporary, as it is undone by way of
1241 side-effecting mutable type variables after simplification and constraint
1242 entailment has been completed.
1243
1244 This version is an (attempt at, yet unproven, an) *unflattened* version of
1245 the SubstL-Ev completion rule.
1246
1247 The above rule is essential to catch non-terminating rules that cannot be
1248 oriented properly, like
1249
1250      F a ~ [G (F a)]
1251  or even
1252      a ~ [G a]          , where a is a skolem tyvar
1253
1254 The left-to-right orientiation is not suitable because it does not
1255 terminate. The right-to-left orientation is not suitable because it
1256 does not have a type-function on the left. This is undesirable because
1257 it would hide information. E.g. assume
1258
1259         instance C [x]
1260
1261 then rewriting C [G (F a)] to C (F a) is bad because we cannot now
1262 see that the C [x] instance applies.
1263
1264 The rule also caters for badly-oriented rules of the form:
1265
1266      F a ~ G (F a)
1267
1268 for which other solutions are possible, but this one will do too.
1269
1270 It's behavior is:
1271
1272   co : ty1 ~ ty2{F ty1}
1273      >-->
1274   co         : ty1 ~ ty2{b}
1275   sym (F co) : F ty2{b} ~ b
1276         where b is a fresh skolem variable
1277
1278 We also cater for the symmetric situation *if* the rule cannot be used as a
1279 left-to-right rewrite rule.
1280
1281 We also return an action (b := ty1) which is used to eliminate b
1282 after the dust of normalisation with the completed rewrite system
1283 has settled.
1284
1285 A subtle point of this transformation is that both coercions in the results
1286 are strictly speaking incorrect.  However, they are correct again after the
1287 action {B := ty1} has removed the skolem again.  This happens immediately
1288 after constraint entailment has been checked; ie, code outside of the
1289 simplification and entailment checking framework will never see these
1290 temporarily incorrect coercions.
1291
1292 NB: We perform this transformation for multiple occurences of ty1 under one
1293     or multiple family applications on the left-hand side at once (ie, the
1294     rule doesn't need to be applied multiple times at a single inst).  As a
1295     result we can get two or more insts back.
1296
1297 Note [skolemOccurs loop]
1298 ~~~~~~~~~~~~~~~~~~~~~~~~
1299 You might think that under
1300
1301   type family F a
1302   type instance F [a] = [F a]
1303
1304 a signature such as
1305
1306   foo :: (F [a] ~ a) => a
1307
1308 will get us into a loop.  However, this is *not* the case.  Here is why:
1309
1310     F [a<sk>] ~ a<sk>
1311
1312     -->(TOP)
1313
1314     [F a<sk>] ~ a<sk>
1315
1316     -->(SkolemOccurs)
1317
1318     [b<tau>] ~ a<sk>
1319     F [b<tau>] ~ b<tau>   , with b := F a
1320
1321     -->(TOP)
1322
1323     [b<tau>] ~ a<sk>
1324     [F b<tau>] ~ b<tau>   , with b := F a
1325
1326 At this point (SkolemOccurs) does *not* apply anymore, as
1327
1328   [F b<tau>] ~ b<tau>
1329
1330 is not used as a rewrite rule.  The variable b<tau> is not a skolem (cf
1331 eqInstToRewrite).
1332
1333 (The regression test indexed-types/should_compile/Simple20 checks that the
1334 described property of the system does not change.)
1335
1336 \begin{code}
1337 skolemOccurs :: PrecondRule
1338 skolemOccurs insts
1339   = do { (instss, undoSkolems) <- mapAndUnzipM oneSkolemOccurs insts
1340        ; return (concat instss, sequence_ undoSkolems)
1341        }
1342   where
1343     oneSkolemOccurs inst
1344       = ASSERT( isEqInst inst )
1345         case eqInstToRewrite inst of
1346           Just (rewrite, swapped) -> breakRecursion rewrite swapped
1347           Nothing                 -> return ([inst], return ())
1348       where
1349         -- inst is an elementary rewrite rule, check whether we need to break
1350         -- it up
1351         breakRecursion (Rewrite pat body _) swapped
1352
1353           -- skolemOccurs does not apply, leave as is
1354           | null tysToLiftOut
1355           = do { traceTc $ text "oneSkolemOccurs: no tys to lift out"
1356                ; return ([inst], return ())
1357                }
1358
1359           -- recursive occurence of pat in body under a type family application
1360           | otherwise
1361           = do { traceTc $ text "oneSkolemOccurs[TLO]:" <+> ppr tysToLiftOut
1362                ; skTvs <- mapM (newMetaTyVar TauTv . typeKind) tysToLiftOut
1363                ; let skTvs_tysTLO   = zip skTvs tysToLiftOut
1364                      insertSkolems = return . replace skTvs_tysTLO
1365                ; (_, body') <- tcGenericNormaliseFamInst insertSkolems body
1366                ; inst' <- if swapped then mkEqInst (EqPred body' pat) co
1367                                      else mkEqInst (EqPred pat body') co
1368                                      -- ensure to reconstruct the inst in the
1369                                      -- original orientation
1370                ; traceTc $ text "oneSkolemOccurs[inst']:" <+> ppr inst'
1371                ; (insts, undoSk) <- mapAndUnzipM (mkSkolemInst inst')
1372                                                  skTvs_tysTLO
1373                ; return (inst':insts, sequence_ undoSk)
1374                }
1375           where
1376             co  = eqInstCoercion inst
1377
1378             -- all subtypes that are (1) type family instances and (2) contain
1379             -- the lhs type as part of the type arguments of the type family
1380             -- constructor
1381             tysToLiftOut = [mkTyConApp tc tys | (tc, tys) <- tyFamInsts body
1382                                               , any (pat `tcPartOfType`) tys]
1383
1384             replace :: [(TcTyVar, Type)] -> Type -> Maybe (Type, Coercion)
1385             replace []                   _  = Nothing
1386             replace ((skTv, tyTLO):rest) ty
1387               | tyTLO `tcEqType` ty         = Just (mkTyVarTy skTv, undefined)
1388               | otherwise                   = replace rest ty
1389
1390             -- create the EqInst for the equality determining the skolem and a
1391             -- TcM action undoing the skolem introduction
1392             mkSkolemInst inst' (skTv, tyTLO)
1393               = do { (co, tyLiftedOut) <- tcEqInstNormaliseFamInst inst' tyTLO
1394                    ; inst <- mkEqInst (EqPred tyLiftedOut (mkTyVarTy skTv))
1395                                       (mkGivenCo $ mkSymCoercion (fromACo co))
1396                                       -- co /= IdCo due to construction of inst'
1397                    ; return (inst, writeMetaTyVar skTv tyTLO)
1398                    }
1399 \end{code}
1400
1401
1402 Removal of trivial equalities: trivialRule
1403 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1404 The following rules exploits the reflexivity of equality:
1405
1406   (Trivial)
1407     g1 : t ~ t
1408       >-->
1409     g1 := t
1410
1411 \begin{code}
1412 trivialRule :: IdemRewriteRule
1413 trivialRule insts
1414   = liftM catMaybes $ mapM trivial insts
1415   where
1416     trivial inst
1417       | ASSERT( isEqInst inst )
1418         ty1 `tcEqType` ty2
1419       = do { eitherEqInst inst
1420                (\cotv -> writeMetaTyVar cotv ty1)
1421                (\_    -> return ())
1422            ; return Nothing
1423            }
1424       | otherwise
1425       = return $ Just inst
1426       where
1427          (ty1,ty2) = eqInstTys inst
1428 \end{code}
1429
1430
1431 Decomposition of data type constructors: decompRule
1432 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1433 Whenever, the same *data* constructors occurs on both sides of an equality, we
1434 can decompose as in standard unification.
1435
1436   (Decomp)
1437     g1 : T cs ~ T ds
1438       >-->
1439     g21 : c1 ~ d1, ..., g2n : cn ~ dn
1440     g1 := T g2s
1441
1442 Works also for the case where T is actually an application of a type family
1443 constructor to a set of types, provided the applications on both sides of the
1444 ~ are identical; see also Note [OpenSynTyCon app] in TcUnify.
1445
1446 We guarantee to raise an error for any inconsistent equalities;
1447 cf Note [Inconsistencies in equality constraints].
1448
1449 \begin{code}
1450 decompRule :: RewriteRule
1451 decompRule insts
1452   = do { (insts, changed) <- mapAndUnzipM decomp insts
1453        ; return (concat insts, or changed)
1454        }
1455   where
1456     decomp inst
1457       = ASSERT( isEqInst inst )
1458         go ty1 ty2
1459       where
1460         (ty1,ty2) = eqInstTys inst
1461         go ty1 ty2
1462           | Just ty1' <- tcView ty1 = go ty1' ty2
1463           | Just ty2' <- tcView ty2 = go ty1 ty2'
1464
1465         go (TyConApp con1 tys1) (TyConApp con2 tys2)
1466           | con1 == con2 && identicalHead
1467           = mkArgInsts (mkTyConApp con1) tys1 tys2
1468
1469           | con1 /= con2 && not (isOpenSynTyCon con1 || isOpenSynTyCon con2)
1470             -- not matching data constructors (of any flavour) are bad news
1471           = eqInstMisMatch inst
1472           where
1473             n             = tyConArity con1
1474             (idxTys1, _)  = splitAt n tys1
1475             (idxTys2, _)  = splitAt n tys2
1476             identicalHead = not (isOpenSynTyCon con1) ||
1477                             idxTys1 `tcEqTypes` idxTys2
1478
1479         go (FunTy fun1 arg1) (FunTy fun2 arg2)
1480           = mkArgInsts (\[funCo, argCo] -> mkFunTy funCo argCo) [fun1, arg1]
1481                                                                 [fun2, arg2]
1482
1483         -- Applications need a bit of care!
1484         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
1485         go (AppTy s1 t1) ty2
1486           | Just (s2, t2) <- tcSplitAppTy_maybe ty2
1487           = mkArgInsts (\[s, t] -> mkAppTy s t) [s1, t1] [s2, t2]
1488
1489         -- Symmetric case
1490         go ty1 (AppTy s2 t2)
1491           | Just (s1, t1) <- tcSplitAppTy_maybe ty1
1492           = mkArgInsts (\[s, t] -> mkAppTy s t) [s1, t1] [s2, t2]
1493
1494         -- We already covered all the consistent cases of rigid types on both
1495         -- sides; so, if we see two rigid types here, we discovered an
1496         -- inconsistency.
1497         go ty1 ty2
1498           | isRigid ty1 && isRigid ty2
1499           = eqInstMisMatch inst
1500
1501         -- We can neither assert consistency nor inconsistency => defer
1502         go _ _ = return ([inst], False)
1503
1504         isRigid (TyConApp con _) = not (isOpenSynTyCon con)
1505         isRigid (FunTy _ _)      = True
1506         isRigid (AppTy _ _)      = True
1507         isRigid _                = False
1508
1509         -- Create insts for matching argument positions (ie, the bit after
1510         -- '>-->' in the rule description above)
1511         mkArgInsts con tys1 tys2
1512           = do { cos <- eitherEqInst inst
1513                           -- old_co := Con1 cos
1514                           (\old_covar ->
1515                             do { cotvs <- zipWithM newMetaCoVar tys1 tys2
1516                                ; let cos = map mkTyVarTy cotvs
1517                                ; writeMetaTyVar old_covar (con cos)
1518                                ; return $ map mkWantedCo cotvs
1519                                })
1520                           -- co_i := Con_i old_co
1521                           (\old_co ->
1522                             return $ map mkGivenCo $
1523                                          mkRightCoercions (length tys1) old_co)
1524                ; insts <- zipWithM mkEqInst (zipWith EqPred tys1 tys2) cos
1525                ; traceTc (text "decomp identicalHead" <+> ppr insts)
1526                ; return (insts, not $ null insts)
1527                }
1528 \end{code}
1529
1530
1531 Rewriting with type instances: topRule
1532 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1533 We use (toplevel) type instances to normalise both sides of equalities.
1534
1535   (Top)
1536     g1 : t ~ s
1537       >--> co1 :: t ~ t' / co2 :: s ~ s'
1538     g2 : t' ~ s'
1539     g1 := co1 * g2 * sym co2
1540
1541 \begin{code}
1542 topRule :: RewriteRule
1543 topRule insts
1544   =  do { (insts, changed) <- mapAndUnzipM top insts
1545         ; return (insts, or changed)
1546         }
1547   where
1548     top inst
1549       = ASSERT( isEqInst inst )
1550         do { (coi1, ty1') <- tcNormaliseFamInst ty1
1551            ; (coi2, ty2') <- tcNormaliseFamInst ty2
1552            ; case (coi1, coi2) of
1553                (IdCo, IdCo) -> return (inst, False)
1554                _            ->
1555                  do { wg_co <-
1556                        eitherEqInst inst
1557                          -- old_co = co1 * new_co * sym co2
1558                          (\old_covar ->
1559                            do { new_cotv <- newMetaCoVar ty1' ty2'
1560                               ; let new_co  = mkTyVarTy new_cotv
1561                                     old_coi = coi1 `mkTransCoI`
1562                                               ACo new_co `mkTransCoI`
1563                                               (mkSymCoI coi2)
1564                               ; writeMetaTyVar old_covar (fromACo old_coi)
1565                               ; return $ mkWantedCo new_cotv
1566                               })
1567                          -- new_co = sym co1 * old_co * co2
1568                          (\old_co ->
1569                            return $
1570                              mkGivenCo $
1571                                fromACo $
1572                                  mkSymCoI coi1 `mkTransCoI`
1573                                  ACo old_co `mkTransCoI` coi2)
1574                    ; new_inst <- mkEqInst (EqPred ty1' ty2') wg_co
1575                    ; return (new_inst, True)
1576                    }
1577              }
1578       where
1579         (ty1,ty2) = eqInstTys inst
1580 \end{code}
1581
1582
1583 Rewriting with equalities: substRule
1584 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1585 From a set of insts, use all insts that can be read as rewrite rules to
1586 rewrite the types in all other insts.
1587
1588   (Subst)
1589     g : F c ~ t,
1590     forall g1 : s1{F c} ~ s2{F c}
1591       >-->
1592     g2 : s1{t} ~ s2{t}
1593     g1 := s1{g} * g2  * sym s2{g}  <=>  g2 := sym s1{g} * g1 * s2{g}
1594
1595 Alternatively, the rewrite rule may have the form (g : a ~ t).
1596
1597 To avoid having to swap rules of the form (g : t ~ F c) and (g : t ~ a),
1598 where t is neither a variable nor a type family application, we use them for
1599 rewriting from right-to-left.  However, it is crucial to only apply rules
1600 from right-to-left if they cannot be used left-to-right.
1601
1602 The workhorse is substInst, which performs an occurs check before actually
1603 using an equality for rewriting.  If the type pattern occurs in the type we
1604 substitute for the pattern, normalisation would diverge.
1605
1606 \begin{code}
1607 substRule :: RewriteRule
1608 substRule insts = tryAllInsts insts []
1609   where
1610     -- for every inst check whether it can be used to rewrite the others
1611     -- (we make an effort to keep the insts in order; it makes debugging
1612     -- easier)
1613     tryAllInsts []           triedInsts = return (reverse triedInsts, False)
1614     tryAllInsts (inst:insts) triedInsts
1615       = do { (insts', changed) <- substInst inst (reverse triedInsts ++ insts)
1616            ; if changed then return (insertAt (length triedInsts) inst insts',
1617                                      True)
1618                         else tryAllInsts insts (inst:triedInsts)
1619            }
1620       where
1621         insertAt n x xs = let (xs1, xs2) = splitAt n xs
1622                           in xs1 ++ [x] ++ xs2
1623
1624 -- Use the given inst as a rewrite rule to normalise the insts in the second
1625 -- argument.  Don't do anything if the inst cannot be used as a rewrite rule,
1626 -- but do apply it right-to-left, if possible, and if it cannot be used
1627 -- left-to-right.
1628 --
1629 substInst :: Inst -> [Inst] -> TcM ([Inst], Bool)
1630 substInst inst insts
1631   = case eqInstToRewrite inst of
1632       Just (rewrite, _) -> substEquality rewrite insts
1633       Nothing           -> return (insts, False)
1634   where
1635     substEquality :: Rewrite            -- elementary rewrite
1636                   -> [Inst]             -- insts to rewrite
1637                   -> TcM ([Inst], Bool)
1638     substEquality eqRule@(Rewrite pat rhs _) insts
1639       | pat `tcPartOfType` rhs      -- occurs check!
1640       = occurCheckErr pat rhs
1641       | otherwise
1642       = do { (insts', changed) <- mapAndUnzipM substOne insts
1643            ; return (insts', or changed)
1644            }
1645       where
1646         substOne inst
1647           = ASSERT( isEqInst inst )
1648             do { (coi1, ty1') <- tcEqRuleNormaliseFamInst eqRule ty1
1649                ; (coi2, ty2') <- tcEqRuleNormaliseFamInst eqRule ty2
1650                ; case (coi1, coi2) of
1651                 (IdCo, IdCo) -> return (inst, False)
1652                 _            ->
1653                   do { gw_co <-
1654                          eitherEqInst inst
1655                            -- old_co := co1 * new_co * sym co2
1656                            (\old_covar ->
1657                              do { new_cotv <- newMetaCoVar ty1' ty2'
1658                                 ; let new_co  = mkTyVarTy new_cotv
1659                                       old_coi = coi1 `mkTransCoI`
1660                                                 ACo new_co `mkTransCoI`
1661                                                 (mkSymCoI coi2)
1662                                 ; writeMetaTyVar old_covar (fromACo old_coi)
1663                                 ; return $ mkWantedCo new_cotv
1664                                 })
1665                            -- new_co := sym co1 * old_co * co2
1666                            (\old_co ->
1667                              return $
1668                                mkGivenCo $
1669                                  fromACo $
1670                                    mkSymCoI coi1 `mkTransCoI`
1671                                    ACo old_co `mkTransCoI` coi2)
1672                      ; new_inst <- mkEqInst (EqPred ty1' ty2') gw_co
1673                      ; return (new_inst, True)
1674                      }
1675                }
1676           where
1677             (ty1,ty2) = eqInstTys inst
1678 \end{code}
1679
1680
1681 Instantiate meta variables: unifyMetaRule
1682 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1683 If an equality equates a meta type variable with a type, we simply instantiate
1684 the meta variable.
1685
1686   (UnifyMeta)
1687     g : alpha ~ t
1688       >-->
1689     alpha := t
1690     g     := t
1691
1692 Meta variables can only appear in wanted constraints, and this rule should
1693 only be applied to wanted constraints.  We also know that t definitely is
1694 distinct from alpha (as the trivialRule) has been run on the insts beforehand.
1695
1696 NB: We cannot assume that meta tyvars are empty.  They may have been updated
1697 by another inst in the currently processed wanted list.  We need to be very
1698 careful when updateing type variables (see TcUnify.uUnfilledVar), but at least
1699 we know that we have no boxes.  It's unclear that it would be an advantage to
1700 common up the code in TcUnify and the code below.  Firstly, we don't want
1701 calls to TcUnify.defer_unification here, and secondly, TcUnify import the
1702 current module, so we would have to move everything here (Yuk!) or to
1703 TcMType.  Besides, the code here is much simpler due to the lack of boxes.
1704
1705 \begin{code}
1706 unifyMetaRule :: RewriteRule
1707 unifyMetaRule insts
1708   = do { (insts', changed) <- mapAndUnzipM unifyMeta insts
1709        ; return (concat insts', or changed)
1710        }
1711   where
1712     unifyMeta inst
1713       = ASSERT( isEqInst inst )
1714         go ty1 ty2
1715            (fromWantedCo "unifyMetaRule" $ eqInstCoercion inst)
1716       where
1717         (ty1,ty2) = eqInstTys inst
1718         go ty1 ty2 cotv
1719           | Just ty1' <- tcView ty1 = go ty1' ty2 cotv
1720           | Just ty2' <- tcView ty2 = go ty1 ty2' cotv
1721
1722           | TyVarTy tv1 <- ty1
1723           , isMetaTyVar tv1         = do { lookupTV <- lookupTcTyVar tv1
1724                                          ; uMeta False tv1 lookupTV ty2 cotv
1725                                          }
1726           | TyVarTy tv2 <- ty2
1727           , isMetaTyVar tv2         = do { lookupTV <- lookupTcTyVar tv2
1728                                          ; uMeta True tv2 lookupTV ty1 cotv
1729                                          }
1730           | otherwise               = return ([inst], False)
1731
1732         -- meta variable has been filled already
1733         -- => ignore this inst (we'll come around again, after zonking)
1734         uMeta _swapped _tv (IndirectTv _) _ty _cotv
1735           = return ([inst], False)
1736
1737         -- type variable meets type variable
1738         -- => check that tv2 hasn't been updated yet and choose which to update
1739         uMeta swapped tv1 (DoneTv details1) (TyVarTy tv2) cotv
1740           | tv1 == tv2
1741           = return ([inst], False)      -- The two types are already identical
1742
1743           | otherwise
1744           = do { lookupTV2 <- lookupTcTyVar tv2
1745                ; case lookupTV2 of
1746                    IndirectTv ty   -> uMeta swapped tv1 (DoneTv details1) ty cotv
1747                    DoneTv details2 -> uMetaVar swapped tv1 details1 tv2 details2 cotv
1748                }
1749
1750         ------ Beyond this point we know that ty2 is not a type variable
1751
1752         -- signature skolem meets non-variable type
1753         -- => cannot update!
1754         uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) _non_tv_ty _cotv
1755           = return ([inst], False)
1756
1757         -- updatable meta variable meets non-variable type
1758         -- => occurs check, monotype check, and kinds match check, then update
1759         uMeta swapped tv (DoneTv (MetaTv _ ref)) non_tv_ty cotv
1760           = do { mb_ty' <- checkTauTvUpdate tv non_tv_ty    -- occurs + monotype check
1761                ; case mb_ty' of
1762                    Nothing  -> return ([inst], False)  -- tv occurs in faminst
1763                    Just ty' ->
1764                      do { checkUpdateMeta swapped tv ref ty'  -- update meta var
1765                         ; writeMetaTyVar cotv ty'             -- update co var
1766                         ; return ([], True)
1767                         }
1768                }
1769
1770         uMeta _ _ _ _ _ = panic "uMeta"
1771
1772         -- uMetaVar: unify two type variables
1773         -- meta variable meets skolem
1774         -- => just update
1775         uMetaVar swapped tv1 (MetaTv _ ref) tv2 (SkolemTv _) cotv
1776           = do { checkUpdateMeta swapped tv1 ref (mkTyVarTy tv2)
1777                ; writeMetaTyVar cotv (mkTyVarTy tv2)
1778                ; return ([], True)
1779                }
1780
1781         -- meta variable meets meta variable
1782         -- => be clever about which of the two to update
1783         --   (from TcUnify.uUnfilledVars minus boxy stuff)
1784         uMetaVar swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) cotv
1785           = do { case (info1, info2) of
1786                    -- Avoid SigTvs if poss
1787                    (SigTv _, _      ) | k1_sub_k2 -> update_tv2
1788                    (_,       SigTv _) | k2_sub_k1 -> update_tv1
1789
1790                    (_,   _) | k1_sub_k2 -> if k2_sub_k1 && nicer_to_update_tv1
1791                                            then update_tv1      -- Same kinds
1792                                            else update_tv2
1793                             | k2_sub_k1 -> update_tv1
1794                             | otherwise -> kind_err
1795               -- Update the variable with least kind info
1796               -- See notes on type inference in Kind.lhs
1797               -- The "nicer to" part only applies if the two kinds are the same,
1798               -- so we can choose which to do.
1799
1800                ; writeMetaTyVar cotv (mkTyVarTy tv2)
1801                ; return ([], True)
1802                }
1803           where
1804                 -- Kinds should be guaranteed ok at this point
1805             update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
1806             update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
1807
1808             kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
1809                        unifyKindMisMatch k1 k2
1810
1811             k1 = tyVarKind tv1
1812             k2 = tyVarKind tv2
1813             k1_sub_k2 = k1 `isSubKind` k2
1814             k2_sub_k1 = k2 `isSubKind` k1
1815
1816             nicer_to_update_tv1 = isSystemName (Var.varName tv1)
1817                 -- Try to update sys-y type variables in preference to ones
1818                 -- gotten (say) by instantiating a polymorphic function with
1819                 -- a user-written type sig
1820
1821         uMetaVar _ _ _ _ _ _ = panic "uMetaVar"
1822 \end{code}
1823
1824
1825 %************************************************************************
1826 %*                                                                      *
1827 \section{Normalisation of Insts}
1828 %*                                                                      *
1829 %************************************************************************
1830
1831 Normalises a set of dictionaries relative to a set of given equalities (which
1832 are interpreted as rewrite rules).  We only consider given equalities of the
1833 form
1834
1835   F ts ~ t    or    a ~ t
1836
1837 where F is a type family.
1838
1839 \begin{code}
1840 substEqInDictInsts :: Bool      -- whether the *dictionaries* are wanted/given
1841                    -> [Inst]    -- given equalities (used as rewrite rules)
1842                    -> [Inst]    -- dictinaries to be normalised
1843                    -> TcM ([Inst], TcDictBinds)
1844 substEqInDictInsts isWanted eqInsts dictInsts
1845   = do { traceTc (text "substEqInDictInst <-" <+> ppr dictInsts)
1846        ; dictInsts' <-
1847            foldlM rewriteWithOneEquality (dictInsts, emptyBag) eqInsts
1848        ; traceTc (text "substEqInDictInst ->" <+> ppr dictInsts')
1849        ; return dictInsts'
1850        }
1851   where
1852       -- (1) Given equality of form 'F ts ~ t' or 'a ~ t': use for rewriting
1853     rewriteWithOneEquality (dictInsts, dictBinds)
1854                            eqInst@(EqInst {tci_left  = pattern,
1855                                            tci_right = target})
1856       | isOpenSynTyConApp pattern || isTyVarTy pattern
1857       = do { (dictInsts', moreDictBinds) <-
1858                genericNormaliseInsts isWanted applyThisEq dictInsts
1859            ; return (dictInsts', dictBinds `unionBags` moreDictBinds)
1860            }
1861       where
1862         applyThisEq = tcGenericNormaliseFamInstPred (return . matchResult)
1863
1864         -- rewrite in case of an exact match
1865         matchResult ty | tcEqType pattern ty = Just (target, eqInstType eqInst)
1866                        | otherwise           = Nothing
1867
1868       -- (2) Given equality has the wrong form: ignore
1869     rewriteWithOneEquality (dictInsts, dictBinds) _not_a_rewrite_rule
1870       = return (dictInsts, dictBinds)
1871 \end{code}
1872
1873
1874 Take a bunch of Insts (not EqInsts), and normalise them wrt the top-level
1875 type-function equations, where
1876
1877         (norm_insts, binds) = normaliseInsts is_wanted insts
1878
1879 If 'is_wanted'
1880   = True,  (binds + norm_insts) defines insts       (wanteds)
1881   = False, (binds + insts)      defines norm_insts  (givens)
1882
1883 Ie, in the case of normalising wanted dictionaries, we use the normalised
1884 dictionaries to define the originally wanted ones.  However, in the case of
1885 given dictionaries, we use the originally given ones to define the normalised
1886 ones.
1887
1888 \begin{code}
1889 normaliseInsts :: Bool                          -- True <=> wanted insts
1890                -> [Inst]                        -- wanted or given insts
1891                -> TcM ([Inst], TcDictBinds)     -- normalised insts and bindings
1892 normaliseInsts isWanted insts
1893   = genericNormaliseInsts isWanted tcNormaliseFamInstPred insts
1894
1895 genericNormaliseInsts  :: Bool                      -- True <=> wanted insts
1896                        -> (TcPredType -> TcM (CoercionI, TcPredType))
1897                                                     -- how to normalise
1898                        -> [Inst]                    -- wanted or given insts
1899                        -> TcM ([Inst], TcDictBinds) -- normalised insts & binds
1900 genericNormaliseInsts isWanted fun insts
1901   = do { (insts', binds) <- mapAndUnzipM (normaliseOneInst isWanted fun) insts
1902        ; return (insts', unionManyBags binds)
1903        }
1904   where
1905     normaliseOneInst isWanted fun
1906                      dict@(Dict {tci_pred = pred,
1907                                  tci_loc  = loc})
1908       = do { traceTc $ text "genericNormaliseInst <-" <+> ppr dict
1909            ; (coi, pred') <- fun pred
1910
1911            ; case coi of
1912                IdCo   ->
1913                  do { traceTc $ text "genericNormaliseInst ->" <+> ppr dict
1914                     ; return (dict, emptyBag)
1915                     }
1916                          -- don't use pred' in this case; otherwise, we get
1917                          -- more unfolded closed type synonyms in error messages
1918                ACo co ->
1919                  do { -- an inst for the new pred
1920                     ; dict' <- newDictBndr loc pred'
1921                       -- relate the old inst to the new one
1922                       -- target_dict = source_dict `cast` st_co
1923                     ; let (target_dict, source_dict, st_co)
1924                             | isWanted  = (dict,  dict', mkSymCoercion co)
1925                             | otherwise = (dict', dict,  co)
1926                               -- we have
1927                               --   co :: dict ~ dict'
1928                               -- hence, if isWanted
1929                               --          dict  = dict' `cast` sym co
1930                               --        else
1931                               --          dict' = dict  `cast` co
1932                           expr      = HsVar $ instToId source_dict
1933                           cast_expr = HsWrap (WpCast st_co) expr
1934                           rhs       = L (instLocSpan loc) cast_expr
1935                           binds     = instToDictBind target_dict rhs
1936                       -- return the new inst
1937                     ; traceTc $ let name | isWanted
1938                                          = "genericNormaliseInst (wanted) ->"
1939                                          | otherwise
1940                                          = "genericNormaliseInst (given) ->"
1941                                 in
1942                                 text name <+> ppr dict' <+>
1943                                 text "with" <+> ppr binds
1944                     ; return (dict', binds)
1945                     }
1946            }
1947
1948         -- TOMDO: What do we have to do about ImplicInst, Method, and LitInst??
1949     normaliseOneInst _isWanted _fun inst
1950       = do { inst' <- zonkInst inst
1951            ; traceTc $ text "*** TcTyFuns.normaliseOneInst: Skipping" <+>
1952                        ppr inst
1953            ; return (inst', emptyBag)
1954            }
1955 \end{code}
1956
1957
1958 %************************************************************************
1959 %*                                                                      *
1960 \section{Errors}
1961 %*                                                                      *
1962 %************************************************************************
1963
1964 The infamous couldn't match expected type soandso against inferred type
1965 somethingdifferent message.
1966
1967 \begin{code}
1968 eqInstMisMatch :: Inst -> TcM a
1969 eqInstMisMatch inst
1970   = ASSERT( isEqInst inst )
1971     setErrCtxt ctxt $ failWithMisMatch ty_act ty_exp
1972   where
1973     (ty_act, ty_exp) = eqInstTys inst
1974     InstLoc _ _ ctxt = instLoc   inst
1975
1976 -----------------------
1977 failWithMisMatch :: TcType -> TcType -> TcM a
1978 -- Generate the message when two types fail to match,
1979 -- going to some trouble to make it helpful.
1980 -- The argument order is: actual type, expected type
1981 failWithMisMatch ty_act ty_exp
1982   = do  { env0 <- tcInitTidyEnv
1983         ; ty_exp <- zonkTcType ty_exp
1984         ; ty_act <- zonkTcType ty_act
1985         ; failWithTcM (misMatchMsg env0 (ty_act, ty_exp))
1986         }
1987
1988 misMatchMsg :: TidyEnv -> (TcType, TcType) -> (TidyEnv, SDoc)
1989 misMatchMsg env0 (ty_act, ty_exp)
1990   = let (env1, pp_exp, extra_exp) = ppr_ty env0 ty_exp
1991         (env2, pp_act, extra_act) = ppr_ty env1 ty_act
1992         msg = sep [sep [ptext (sLit "Couldn't match expected type") <+> pp_exp,
1993                         nest 7 $
1994                               ptext (sLit "against inferred type") <+> pp_act],
1995                    nest 2 (extra_exp $$ extra_act)]
1996     in
1997     (env2, msg)
1998
1999   where
2000     ppr_ty :: TidyEnv -> TcType -> (TidyEnv, SDoc, SDoc)
2001     ppr_ty env ty
2002       = let (env1, tidy_ty) = tidyOpenType env ty
2003             (env2, extra)  = ppr_extra env1 tidy_ty
2004         in
2005         (env2, quotes (ppr tidy_ty), extra)
2006
2007     -- (ppr_extra env ty) shows extra info about 'ty'
2008     ppr_extra :: TidyEnv -> Type -> (TidyEnv, SDoc)
2009     ppr_extra env (TyVarTy tv)
2010       | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv) && not (isUnk tv)
2011       = (env1, pprSkolTvBinding tv1)
2012       where
2013         (env1, tv1) = tidySkolemTyVar env tv
2014
2015     ppr_extra env _ty = (env, empty)            -- Normal case
2016 \end{code}