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