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