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