compiler/typecheck/TcTyFuns.lhs

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