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