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