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 {   -- try the SubstFam rule
 888              optEqs <- applySubstFam eq1 eq2
 889            ; case optEqs of
 890                Just (eqs, skolems) -> return (eqs, [], skolems)
 891                Nothing             -> do
 892            {   -- try the SubstVarVar rule
 893              optEqs <- applySubstVarVar eq1 eq2
 894            ; case optEqs of
 895                Just (eqs, skolems) -> return (eqs, [], skolems)
 896                Nothing             -> do
 897            {   -- try the SubstVarFam rule
 898              optEqs <- applySubstVarFam eq1 eq2
 899            ; case optEqs of
 900                Just eq -> return ([eq], [], emptyVarSet)
 901                Nothing -> return ([], [eq2], emptyVarSet)
 902                  -- if no rule matches, we return the equlity we tried to
 903                  -- substitute into unchanged
 904            }}}
 905 \end{code}
 906
 907 Attempt to apply the Top rule.  The rule is
 908
 909   co :: F t1..tn ~ t
 910   =(Top)=>
 911   co' :: [s1/x1, .., sm/xm]s ~ t with co = g s1..sm |> co'
 912
 913 where g :: forall x1..xm. F u1..um ~ s and [s1/x1, .., sm/xm]u1 == t1.
 914
 915 Returns Nothing if the rule could not be applied.  Otherwise, the resulting
 916 equality is normalised and a list of the normal equalities is returned.
 917
 918 \begin{code}
 919 applyTop :: RewriteInst -> TcM (Maybe ([RewriteInst], TyVarSet))
 920
 921 applyTop eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
 922   = do { optTyCo <- tcUnfoldSynFamInst (TyConApp fam args)
 923        ; case optTyCo of
 924            Nothing                -> return Nothing
 925            Just (lhs, rewrite_co)
 926              -> do { co' <- mkRightTransEqInstCo co rewrite_co (lhs, rhs)
 927                    ; eq' <- deriveEqInst eq lhs rhs co'
 928                    ; liftM Just $ normEqInst eq'
 929                    }
 930        }
 931   where
 932     co  = rwi_co eq
 933     rhs = rwi_right eq
 934
 935 applyTop _ = return Nothing
 936 \end{code}
 937
 938 Attempt to apply the SubstFam rule.  The rule is
 939
 940   co1 :: F t1..tn ~ t  &  co2 :: F t1..tn ~ s
 941   =(SubstFam)=>
 942   co1 :: F t1..tn ~ t  &  co2' :: t ~ s with co2 = co1 |> co2'
 943
 944 where co1 may be a wanted only if co2 is a wanted, too.
 945
 946 Returns Nothing if the rule could not be applied.  Otherwise, the equality
 947 co2' is normalised and a list of the normal equalities is returned.  (The
 948 equality co1 is not returned as it remain unaltered.)
 949
 950 \begin{code}
 951 applySubstFam :: RewriteInst
 952               -> RewriteInst
 953               -> TcM (Maybe ([RewriteInst], TyVarSet))
 954 applySubstFam eq1@(RewriteFam {rwi_fam = fam1, rwi_args = args1})
 955               eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
 956   | fam1 == fam2 && tcEqTypes args1 args2 &&
 957     (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
 958 -- !!!TODO: tcEqTypes is insufficient as it does not look through type synonyms
 959 -- !!!Check whether anything breaks by making tcEqTypes look through synonyms.
 960 -- !!!Should be ok and we don't want three type equalities.
 961   = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
 962        ; eq2' <- deriveEqInst eq2 lhs rhs co2'
 963        ; liftM Just $ normEqInst eq2'
 964        }
 965   where
 966     lhs = rwi_right eq1
 967     rhs = rwi_right eq2
 968     co1 = eqInstCoType (rwi_co eq1)
 969     co2 = rwi_co eq2
 970 applySubstFam _ _ = return Nothing
 971 \end{code}
 972
 973 Attempt to apply the SubstVarVar rule.  The rule is
 974
 975   co1 :: x ~ t  &  co2 :: x ~ s
 976   =(SubstVarVar)=>
 977   co1 :: x ~ t  &  co2' :: t ~ s with co2 = co1 |> co2'
 978
 979 where co1 may be a wanted only if co2 is a wanted, too.
 980
 981 Returns Nothing if the rule could not be applied.  Otherwise, the equality
 982 co2' is normalised and a list of the normal equalities is returned.  (The
 983 equality co1 is not returned as it remain unaltered.)
 984
 985 \begin{code}
 986 applySubstVarVar :: RewriteInst
 987                  -> RewriteInst
 988                  -> TcM (Maybe ([RewriteInst], TyVarSet))
 989 applySubstVarVar eq1@(RewriteVar {rwi_var = tv1})
 990                  eq2@(RewriteVar {rwi_var = tv2})
 991   | tv1 == tv2 &&
 992     (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
 993   = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
 994        ; eq2' <- deriveEqInst eq2 lhs rhs co2'
 995        ; liftM Just $ normEqInst eq2'
 996        }
 997   where
 998     lhs = rwi_right eq1
 999     rhs = rwi_right eq2
1000     co1 = eqInstCoType (rwi_co eq1)
1001     co2 = rwi_co eq2
1002 applySubstVarVar _ _ = return Nothing
1003 \end{code}
1004
1005 Attempt to apply the SubstVarFam rule.  The rule is
1006
1007   co1 :: x ~ t  &  co2 :: F s1..sn ~ s
1008   =(SubstVarFam)=>
1009   co1 :: x ~ t  &  co2' :: [t/x](F s1..sn) ~ s
1010     with co2 = [co1/x](F s1..sn) |> co2'
1011
1012 where x occurs in F s1..sn. (co1 may be local or wanted.)
1013
1014 Returns Nothing if the rule could not be applied.  Otherwise, the equality
1015 co2' is returned.  (The equality co1 is not returned as it remain unaltered.)
1016
1017 \begin{code}
1018 applySubstVarFam :: RewriteInst -> RewriteInst -> TcM (Maybe RewriteInst)
1019 applySubstVarFam eq1@(RewriteVar {rwi_var = tv1})
1020                  eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
1021   | tv1 `elemVarSet` tyVarsOfTypes args2
1022   = do { let co1Subst = substTyWith [tv1] [co1] (mkTyConApp fam2 args2)
1023              args2'   = substTysWith [tv1] [rhs1] args2
1024              lhs2     = mkTyConApp fam2 args2'
1025        ; co2' <- mkRightTransEqInstCo co2 co1Subst (lhs2, rhs2)
1026        ; return $ Just (eq2 {rwi_args = args2', rwi_co = co2'})
1027        }
1028   where
1029     rhs1 = rwi_right eq1
1030     rhs2 = rwi_right eq2
1031     co1  = eqInstCoType (rwi_co eq1)
1032     co2  = rwi_co eq2
1033 applySubstVarFam _ _ = return Nothing
1034 \end{code}
1035
1036
1037 %************************************************************************
1038 %*                                                                      *
1039                 Finalisation of equalities
1040 %*                                                                      *
1041 %************************************************************************
1042
1043 Exhaustive substitution of all variable equalities of the form co :: x ~ t
1044 (both local and wanted) into the left-hand sides of all other equalities.  This
1045 may lead to recursive equalities; i.e., (1) we need to apply the substitution
1046 implied by one variable equality exhaustively before turning to the next and
1047 (2) we need an occurs check.
1048
1049 We also apply the same substitutions to the local and wanted class and IP
1050 dictionaries.
1051
1052 The treatment of flexibles in wanteds is quite subtle.  We absolutely want to
1053 substitute them into right-hand sides of equalities, to avoid getting two
1054 competing instantiations for a type variables; e.g., consider
1055
1056   F s ~ alpha, alpha ~ t
1057
1058 If we don't substitute `alpha ~ t', we may instantiate t with `F s' instead.
1059 This would be bad as `F s' is less useful, eg, as an argument to a class
1060 constraint.
1061
1062 However, there is no reason why we would want to *substitute* `alpha ~ t' into a
1063 class constraint.  We rather wait until `alpha' is instantiated to `t` and
1064 save the extra dictionary binding that substitution would introduce.
1065 Moreover, we may substitute wanted equalities only into wanted dictionaries.
1066
1067 NB:
1068 * Given that we apply the substitution corresponding to a single equality
1069   exhaustively, before turning to the next, and because we eliminate recursive
1070   equalities, all opportunities for subtitution will have been exhausted after
1071   we have considered each equality once.
1072
1073 \begin{code}
1074 substitute :: [RewriteInst]       -- equalities
1075            -> [Inst]              -- local class dictionaries
1076            -> [Inst]              -- wanted class dictionaries
1077            -> TcM ([RewriteInst], -- equalities after substitution
1078                    TcDictBinds,   -- all newly generated dictionary bindings
1079                    [Inst],        -- local dictionaries after substitution
1080                    [Inst])        -- wanted dictionaries after substitution
1081 substitute eqs locals wanteds = subst eqs [] emptyBag locals wanteds
1082   where
1083     subst [] res binds locals wanteds
1084       = return (res, binds, locals, wanteds)
1085
1086     subst (eq@(RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}):eqs)
1087           res binds locals wanteds
1088       = do { traceTc $ ptext (sLit "TcTyFuns.substitute:") <+> ppr eq
1089
1090            ; let coSubst = zipOpenTvSubst [tv] [eqInstCoType co]
1091                  tySubst = zipOpenTvSubst [tv] [ty]
1092            ; eqs' <- mapM (substEq eq coSubst tySubst) eqs
1093            ; res' <- mapM (substEq eq coSubst tySubst) res
1094
1095              -- only susbtitute local equalities into local dictionaries
1096            ; (lbinds, locals')  <- if not (isWantedCo co)
1097                                    then
1098                                      mapAndUnzipM
1099                                        (substDict eq coSubst tySubst False)
1100                                        locals
1101                                    else
1102                                      return ([], locals)
1103
1104               -- flexible tvs in wanteds will be instantiated anyway, there is
1105               -- no need to substitute them into dictionaries
1106            ; (wbinds, wanteds') <- if not (isMetaTyVar tv && isWantedCo co)
1107                                    then
1108                                      mapAndUnzipM
1109                                        (substDict eq coSubst tySubst True)
1110                                        wanteds
1111                                    else
1112                                      return ([], wanteds)
1113
1114            ; let binds' = unionManyBags $ binds : lbinds ++ wbinds
1115            ; subst eqs' (eq:res') binds' locals' wanteds'
1116            }
1117     subst (eq:eqs) res binds locals wanteds
1118       = subst eqs (eq:res) binds locals wanteds
1119
1120       -- We have, co :: tv ~ ty
1121       -- => apply [ty/tv] to right-hand side of eq2
1122       --    (but only if tv actually occurs in the right-hand side of eq2)
1123     substEq (RewriteVar {rwi_var = tv, rwi_right = ty})
1124             coSubst tySubst eq2
1125       | tv `elemVarSet` tyVarsOfType (rwi_right eq2)
1126       = do { let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
1127                  right2'  = substTy tySubst (rwi_right eq2)
1128                  left2    = case eq2 of
1129                               RewriteVar {rwi_var = tv2}   -> mkTyVarTy tv2
1130                               RewriteFam {rwi_fam = fam,
1131                                           rwi_args = args} ->mkTyConApp fam args
1132            ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2')
1133            ; case eq2 of
1134                RewriteVar {rwi_var = tv2} | tv2 `elemVarSet` tyVarsOfType ty
1135                  -> occurCheckErr left2 right2'
1136                _ -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
1137            }
1138
1139       -- unchanged
1140     substEq _ _ _ eq2
1141       = return eq2
1142
1143       -- We have, co :: tv ~ ty
1144       -- => apply [ty/tv] to dictionary predicate
1145       --    (but only if tv actually occurs in the predicate)
1146     substDict (RewriteVar {rwi_var = tv}) coSubst tySubst isWanted dict
1147       | isClassDict dict
1148       , tv `elemVarSet` tyVarsOfPred (tci_pred dict)
1149       = do { let co1Subst = PredTy (substPred coSubst (tci_pred dict))
1150                  pred'    = substPred tySubst (tci_pred dict)
1151            ; (dict', binds) <- mkDictBind dict isWanted co1Subst pred'
1152            ; return (binds, dict')
1153            }
1154
1155       -- unchanged
1156     substDict _ _ _ _ dict
1157       = return (emptyBag, dict)
1158 -- !!!TODO: Still need to substitute into IP constraints.
1159 \end{code}
1160
1161 For any *wanted* variable equality of the form co :: alpha ~ t or co :: a ~
1162 alpha, we instantiate alpha with t or a, respectively, and set co := id.
1163 Return all remaining wanted equalities.  The Boolean result component is True
1164 if at least one instantiation of a flexible that is *not* a skolem from
1165 flattening was performed.
1166
1167 \begin{code}
1168 instantiateAndExtract :: [RewriteInst] -> Bool -> TyVarSet -> TcM ([Inst], Bool)
1169 instantiateAndExtract eqs localsEmpty skolems
1170   = do { traceTc $ hang (ptext (sLit "instantiateAndExtract:"))
1171                      4 (ppr eqs $$ ppr skolems)
1172        ; results <- mapM inst wanteds
1173        ; let residuals    = [eq | Left eq <- results]
1174              only_skolems = and [tv `elemVarSet` skolems | Right tv <- results]
1175        ; residuals' <- mapM rewriteInstToInst residuals
1176        ; return (residuals', not only_skolems)
1177        }
1178   where
1179     wanteds      = filter (isWantedCo . rwi_co) eqs
1180     checkingMode = length eqs > length wanteds || not localsEmpty
1181                      -- no local equalities or dicts => checking mode
1182
1183         -- co :: alpha ~ t or co :: a ~ alpha
1184     inst eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co})
1185       = do { flexi_tv1       <- isFlexible tv1
1186            ; maybe_flexi_tv2 <- isFlexibleTy ty2
1187            ; case (flexi_tv1, maybe_flexi_tv2) of
1188                (True, _)
1189                  -> -- co :: alpha ~ t
1190                     doInst (rwi_swapped eq) tv1 ty2 co eq
1191                (False, Just tv2)
1192                  -> -- co :: a ~ alpha
1193                     doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
1194                _ -> return $ Left eq
1195            }
1196
1197         -- co :: F args ~ alpha, and we are in checking mode (ie, no locals)
1198     inst eq@(RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = ty2,
1199                          rwi_co = co})
1200       | Just tv2 <- tcGetTyVar_maybe ty2
1201       , isMetaTyVar tv2
1202       , checkingMode || tv2 `elemVarSet` skolems
1203                         -- !!!TODO: this is too liberal, even if tv2 is in
1204                         -- skolems we shouldn't instantiate if tvs occurs
1205                         -- in other equalities that may propagate it into the
1206                         -- environment
1207       = doInst (not $ rwi_swapped eq) tv2 (mkTyConApp fam args) co eq
1208
1209     inst eq = return $ Left eq
1210
1211     -- tv is a meta var and not filled
1212     isFlexible tv
1213       | isMetaTyVar tv = liftM isFlexi $ readMetaTyVar tv
1214       | otherwise      = return False
1215
1216     -- type is a tv that is a meta var and not filled
1217     isFlexibleTy ty
1218       | Just tv <- tcGetTyVar_maybe ty = do {flexi <- isFlexible tv
1219                                             ; if flexi then return $ Just tv
1220                                                        else return Nothing
1221                                             }
1222       | otherwise                      = return Nothing
1223
1224     doInst _swapped _tv _ty (Right ty) _eq
1225       = pprPanic "TcTyFuns.doInst: local eq: " (ppr ty)
1226     doInst swapped tv ty (Left cotv) eq
1227       = do { lookupTV <- lookupTcTyVar tv
1228            ; uMeta swapped tv lookupTV ty cotv
1229            }
1230       where
1231         -- meta variable has been filled already
1232         -- => keep the equality
1233         uMeta _swapped tv (IndirectTv fill_ty) ty _cotv
1234           = do { traceTc $
1235                    ptext (sLit "flexible") <+> ppr tv <+>
1236                    ptext (sLit "already filled with") <+> ppr fill_ty <+>
1237                    ptext (sLit "meant to fill with") <+> ppr ty
1238                ; return $ Left eq
1239                }
1240
1241         -- type variable meets type variable
1242         -- => check that tv2 hasn't been updated yet and choose which to update
1243         uMeta swapped tv1 (DoneTv details1) (TyVarTy tv2) cotv
1244           | tv1 == tv2
1245           = panic "TcTyFuns.uMeta: normalisation shouldn't allow x ~ x"
1246
1247           | otherwise
1248           = do { lookupTV2 <- lookupTcTyVar tv2
1249                ; case lookupTV2 of
1250                    IndirectTv ty   ->
1251                      uMeta swapped tv1 (DoneTv details1) ty cotv
1252                    DoneTv details2 ->
1253                      uMetaVar swapped tv1 details1 tv2 details2 cotv
1254                }
1255
1256         ------ Beyond this point we know that ty2 is not a type variable
1257
1258         -- signature skolem meets non-variable type
1259         -- => cannot update (retain the equality)!
1260         uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) _non_tv_ty _cotv
1261           = return $ Left eq
1262
1263         -- updatable meta variable meets non-variable type
1264         -- => occurs check, monotype check, and kinds match check, then update
1265         uMeta swapped tv (DoneTv (MetaTv _ ref)) non_tv_ty cotv
1266           = do {   -- occurs + monotype check
1267                ; mb_ty' <- checkTauTvUpdate tv non_tv_ty
1268
1269                ; case mb_ty' of
1270                    Nothing  ->
1271                      -- normalisation shouldn't leave families in non_tv_ty
1272                      panic "TcTyFuns.uMeta: unexpected synonym family"
1273                    Just ty' ->
1274                      do { checkUpdateMeta swapped tv ref ty'  -- update meta var
1275                         ; writeMetaTyVar cotv ty'             -- update co var
1276                         ; return $ Right tv
1277                         }
1278                }
1279
1280         uMeta _ _ _ _ _ = panic "TcTyFuns.uMeta"
1281
1282         -- uMetaVar: unify two type variables
1283         -- meta variable meets skolem
1284         -- => just update
1285         uMetaVar swapped tv1 (MetaTv _ ref) tv2 (SkolemTv _) cotv
1286           = do { checkUpdateMeta swapped tv1 ref (mkTyVarTy tv2)
1287                ; writeMetaTyVar cotv (mkTyVarTy tv2)
1288                ; return $ Right tv1
1289                }
1290
1291         -- meta variable meets meta variable
1292         -- => be clever about which of the two to update
1293         --   (from TcUnify.uUnfilledVars minus boxy stuff)
1294         uMetaVar swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) cotv
1295           = do { tv <- case (info1, info2) of
1296                          -- Avoid SigTvs if poss
1297                          (SigTv _, _      ) | k1_sub_k2 -> update_tv2
1298                          (_,       SigTv _) | k2_sub_k1 -> update_tv1
1299
1300                          (_,   _) | k1_sub_k2 -> if k2_sub_k1 &&
1301                                                     nicer_to_update_tv1
1302                                                  then update_tv1  -- Same kinds
1303                                                  else update_tv2
1304                                   | k2_sub_k1 -> update_tv1
1305                                   | otherwise -> kind_err >> return tv1
1306               -- Update the variable with least kind info
1307               -- See notes on type inference in Kind.lhs
1308               -- The "nicer to" part only applies if the two kinds are the same,
1309               -- so we can choose which to do.
1310
1311                ; writeMetaTyVar cotv (mkTyVarTy tv2)
1312                ; return $ Right tv
1313                }
1314           where
1315                 -- Kinds should be guaranteed ok at this point
1316             update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
1317                          >> return tv1
1318             update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
1319                          >> return tv2
1320
1321             kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
1322                        unifyKindMisMatch k1 k2
1323
1324             k1 = tyVarKind tv1
1325             k2 = tyVarKind tv2
1326             k1_sub_k2 = k1 `isSubKind` k2
1327             k2_sub_k1 = k2 `isSubKind` k1
1328
1329             nicer_to_update_tv1 = isSystemName (Var.varName tv1)
1330                 -- Try to update sys-y type variables in preference to ones
1331                 -- gotten (say) by instantiating a polymorphic function with
1332                 -- a user-written type sig
1333
1334         uMetaVar _ _ _ _ _ _ = panic "uMetaVar"
1335 \end{code}
1336
1337
1338 %************************************************************************
1339 %*                                                                      *
1340 \section{Errors}
1341 %*                                                                      *
1342 %************************************************************************
1343
1344 The infamous couldn't match expected type soandso against inferred type
1345 somethingdifferent message.
1346
1347 \begin{code}
1348 eqInstMisMatch :: Inst -> TcM a
1349 eqInstMisMatch inst
1350   = ASSERT( isEqInst inst )
1351     setErrCtxt ctxt $ failWithMisMatch ty_act ty_exp
1352   where
1353     (ty_act, ty_exp) = eqInstTys inst
1354     InstLoc _ _ ctxt = instLoc   inst
1355
1356 -----------------------
1357 failWithMisMatch :: TcType -> TcType -> TcM a
1358 -- Generate the message when two types fail to match,
1359 -- going to some trouble to make it helpful.
1360 -- The argument order is: actual type, expected type
1361 failWithMisMatch ty_act ty_exp
1362   = do  { env0 <- tcInitTidyEnv
1363         ; ty_exp <- zonkTcType ty_exp
1364         ; ty_act <- zonkTcType ty_act
1365         ; failWithTcM (misMatchMsg env0 (ty_act, ty_exp))
1366         }
1367
1368 misMatchMsg :: TidyEnv -> (TcType, TcType) -> (TidyEnv, SDoc)
1369 misMatchMsg env0 (ty_act, ty_exp)
1370   = let (env1, pp_exp, extra_exp) = ppr_ty env0 ty_exp
1371         (env2, pp_act, extra_act) = ppr_ty env1 ty_act
1372         msg = sep [sep [ptext (sLit "Couldn't match expected type") <+> pp_exp,
1373                         nest 7 $
1374                               ptext (sLit "against inferred type") <+> pp_act],
1375                    nest 2 (extra_exp $$ extra_act)]
1376     in
1377     (env2, msg)
1378
1379   where
1380     ppr_ty :: TidyEnv -> TcType -> (TidyEnv, SDoc, SDoc)
1381     ppr_ty env ty
1382       = let (env1, tidy_ty) = tidyOpenType env ty
1383             (env2, extra)  = ppr_extra env1 tidy_ty
1384         in
1385         (env2, quotes (ppr tidy_ty), extra)
1386
1387     -- (ppr_extra env ty) shows extra info about 'ty'
1388     ppr_extra :: TidyEnv -> Type -> (TidyEnv, SDoc)
1389     ppr_extra env (TyVarTy tv)
1390       | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv) && not (isUnk tv)
1391       = (env1, pprSkolTvBinding tv1)
1392       where
1393         (env1, tv1) = tidySkolemTyVar env tv
1394
1395     ppr_extra env _ty = (env, empty)            -- Normal case
1396 \end{code}
1397
1398 Warn of loopy local equalities that were dropped.
1399
1400 \begin{code}
1401 warnDroppingLoopyEquality :: TcType -> TcType -> TcM ()
1402 warnDroppingLoopyEquality ty1 ty2
1403   = do { env0 <- tcInitTidyEnv
1404        ; ty1 <- zonkTcType ty1
1405        ; ty2 <- zonkTcType ty2
1406        ; let (env1 , tidy_ty1) = tidyOpenType env0 ty1
1407              (_env2, tidy_ty2) = tidyOpenType env1 ty2
1408        ; addWarnTc $ hang (ptext (sLit "Dropping loopy given equality"))
1409                        2 (quotes (ppr tidy_ty1 <+> text "~" <+> ppr tidy_ty2))
1410        }
1411 \end{code}