compiler/typecheck/TcTyFuns.lhs

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