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