compiler/typecheck/TcTyFuns.lhs

   1
   2 \begin{code}
   3 {-# OPTIONS -w #-}
   4 -- The above warning supression flag is a temporary kludge.
   5 -- While working on this module you are encouraged to remove it and fix
   6 -- any warnings in the module. See
   7 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
   8 -- for details
   9
  10 module TcTyFuns(
  11         tcNormalizeFamInst,
  12
  13         normaliseGivens, normaliseGivenDicts,
  14         normaliseWanteds, normaliseWantedDicts,
  15         solveWanteds,
  16         substEqInDictInsts,
  17
  18         addBind                 -- should not be here
  19   ) where
  20
  21
  22 #include "HsVersions.h"
  23
  24 import HsSyn
  25
  26 import TcRnMonad
  27 import TcEnv
  28 import Inst
  29 import FamInstEnv
  30 import TcType
  31 import TcMType
  32 import Coercion
  33 import TypeRep  ( Type(..) )
  34 import TyCon
  35 import Var      ( mkCoVar, isTcTyVar )
  36 import Type
  37 import HscTypes ( ExternalPackageState(..) )
  38 import Bag
  39 import Outputable
  40 import SrcLoc   ( Located(..) )
  41 import Maybes
  42
  43 import Data.List
  44 import Control.Monad (liftM)
  45 \end{code}
  46
  47
  48 %************************************************************************
  49 %*                                                                      *
  50                 Normalisation of types
  51 %*                                                                      *
  52 %************************************************************************
  53
  54 Unfold a single synonym family instance and yield the witnessing coercion.
  55 Return 'Nothing' if the given type is either not synonym family instance
  56 or is a synonym family instance that has no matching instance declaration.
  57 (Applies only if the type family application is outermost.)
  58
  59 For example, if we have
  60
  61   :Co:R42T a :: T [a] ~ :R42T a
  62
  63 then 'T [Int]' unfolds to (:R42T Int, :Co:R42T Int).
  64
  65 \begin{code}
  66 tcUnfoldSynFamInst :: Type -> TcM (Maybe (Type, Coercion))
  67 tcUnfoldSynFamInst (TyConApp tycon tys)
  68   | not (isOpenSynTyCon tycon)     -- unfold *only* _synonym_ family instances
  69   = return Nothing
  70   | otherwise
  71   = do { maybeFamInst <- tcLookupFamInst tycon tys
  72        ; case maybeFamInst of
  73            Nothing                -> return Nothing
  74            Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc rep_tys,
  75                                                     mkTyConApp coe_tc rep_tys)
  76              where
  77                coe_tc = expectJust "TcTyFun.tcUnfoldSynFamInst"
  78                                    (tyConFamilyCoercion_maybe rep_tc)
  79        }
  80 tcUnfoldSynFamInst _other = return Nothing
  81 \end{code}
  82
  83 Normalise 'Type's and 'PredType's by unfolding type family applications where
  84 possible (ie, we treat family instances as a TRS).  Also zonk meta variables.
  85
  86         tcNormalizeFamInst ty = (co, ty')
  87         then   co : ty ~ ty'
  88
  89 \begin{code}
  90 tcNormalizeFamInst :: Type -> TcM (CoercionI, Type)
  91 tcNormalizeFamInst = tcGenericNormalizeFamInst tcUnfoldSynFamInst
  92
  93 tcNormalizeFamInstPred :: TcPredType -> TcM (CoercionI, TcPredType)
  94 tcNormalizeFamInstPred = tcGenericNormalizeFamInstPred tcUnfoldSynFamInst
  95 \end{code}
  96
  97 Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
  98 apply the normalisation function gives as the first argument to every TyConApp
  99 and every TyVarTy subterm.
 100
 101         tcGenericNormalizeFamInst fun ty = (co, ty')
 102         then   co : ty ~ ty'
 103
 104 This function is (by way of using smart constructors) careful to ensure that
 105 the returned coercion is exactly IdCo (and not some semantically equivalent,
 106 but syntactically different coercion) whenever (ty' `tcEqType` ty).  This
 107 makes it easy for the caller to determine whether the type changed.  BUT
 108 even if we return IdCo, ty' may be *syntactically* different from ty due to
 109 unfolded closed type synonyms (by way of tcCoreView).  In the interest of
 110 good error messages, callers should discard ty' in favour of ty in this case.
 111
 112 \begin{code}
 113 tcGenericNormalizeFamInst :: (TcType -> TcM (Maybe (TcType,Coercion)))
 114                              -- what to do with type functions and tyvars
 115                            -> TcType                    -- old type
 116                            -> TcM (CoercionI, Type)     -- (coercion, new type)
 117 tcGenericNormalizeFamInst fun ty
 118   | Just ty' <- tcView ty = tcGenericNormalizeFamInst fun ty'
 119 tcGenericNormalizeFamInst fun ty@(TyConApp tyCon tys)
 120   = do  { (cois, ntys) <- mapAndUnzipM (tcGenericNormalizeFamInst fun) tys
 121         ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
 122         ; maybe_ty_co <- fun (TyConApp tyCon ntys)      -- use normalised args!
 123         ; case maybe_ty_co of
 124             -- a matching family instance exists
 125             Just (ty', co) ->
 126               do { let first_coi = mkTransCoI tycon_coi (ACo co)
 127                  ; (rest_coi, nty) <- tcGenericNormalizeFamInst fun ty'
 128                  ; let fix_coi = mkTransCoI first_coi rest_coi
 129                  ; return (fix_coi, nty)
 130                  }
 131             -- no matching family instance exists
 132             -- we do not do anything
 133             Nothing -> return (tycon_coi, TyConApp tyCon ntys)
 134         }
 135 tcGenericNormalizeFamInst fun ty@(AppTy ty1 ty2)
 136   = do  { (coi1,nty1) <- tcGenericNormalizeFamInst fun ty1
 137         ; (coi2,nty2) <- tcGenericNormalizeFamInst fun ty2
 138         ; return (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2)
 139         }
 140 tcGenericNormalizeFamInst fun ty@(FunTy ty1 ty2)
 141   = do  { (coi1,nty1) <- tcGenericNormalizeFamInst fun ty1
 142         ; (coi2,nty2) <- tcGenericNormalizeFamInst fun ty2
 143         ; return (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2)
 144         }
 145 tcGenericNormalizeFamInst fun ty@(ForAllTy tyvar ty1)
 146   = do  { (coi,nty1) <- tcGenericNormalizeFamInst fun ty1
 147         ; return (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
 148         }
 149 tcGenericNormalizeFamInst fun ty@(NoteTy note ty1)
 150   = do  { (coi,nty1) <- tcGenericNormalizeFamInst fun ty1
 151         ; return (mkNoteTyCoI note coi,NoteTy note nty1)
 152         }
 153 tcGenericNormalizeFamInst fun ty@(TyVarTy tv)
 154   | isTcTyVar tv
 155   = do  { traceTc (text "tcGenericNormalizeFamInst" <+> ppr ty)
 156         ; res <- lookupTcTyVar tv
 157         ; case res of
 158             DoneTv _ ->
 159               do { maybe_ty' <- fun ty
 160                  ; case maybe_ty' of
 161                      Nothing         -> return (IdCo, ty)
 162                      Just (ty', co1) ->
 163                        do { (coi2, ty'') <- tcGenericNormalizeFamInst fun ty'
 164                           ; return (ACo co1 `mkTransCoI` coi2, ty'')
 165                           }
 166                  }
 167             IndirectTv ty' -> tcGenericNormalizeFamInst fun ty'
 168         }
 169   | otherwise
 170   = return (IdCo, ty)
 171 tcGenericNormalizeFamInst fun (PredTy predty)
 172   = do  { (coi, pred') <- tcGenericNormalizeFamInstPred fun predty
 173         ; return (coi, PredTy pred') }
 174
 175 ---------------------------------
 176 tcGenericNormalizeFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
 177                               -> TcPredType
 178                               -> TcM (CoercionI, TcPredType)
 179
 180 tcGenericNormalizeFamInstPred fun (ClassP cls tys)
 181   = do { (cois, tys')<- mapAndUnzipM (tcGenericNormalizeFamInst fun) tys
 182        ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
 183        }
 184 tcGenericNormalizeFamInstPred fun (IParam ipn ty)
 185   = do { (coi, ty') <- tcGenericNormalizeFamInst fun ty
 186        ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
 187        }
 188 tcGenericNormalizeFamInstPred fun (EqPred ty1 ty2)
 189   = do { (coi1, ty1') <- tcGenericNormalizeFamInst fun ty1
 190        ; (coi2, ty2') <- tcGenericNormalizeFamInst fun ty2
 191        ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
 192 \end{code}
 193
 194
 195 %************************************************************************
 196 %*                                                                      *
 197 \section{Normalisation of Given Dictionaries}
 198 %*                                                                      *
 199 %************************************************************************
 200
 201 \begin{code}
 202 normaliseGivenDicts, normaliseWantedDicts
 203         :: [Inst]               -- given equations
 204         -> [Inst]               -- dictionaries
 205         -> TcM ([Inst],TcDictBinds)
 206
 207 normaliseGivenDicts  eqs dicts = normalise_dicts eqs dicts False
 208 normaliseWantedDicts eqs dicts = normalise_dicts eqs dicts True
 209
 210 normalise_dicts
 211         :: [Inst]       -- given equations
 212         -> [Inst]       -- dictionaries
 213         -> Bool         -- True <=> the dicts are wanted
 214                         -- Fals <=> they are given
 215         -> TcM ([Inst],TcDictBinds)
 216 normalise_dicts given_eqs dicts is_wanted
 217   = do  { traceTc $ text "normaliseGivenDicts <-" <+> ppr dicts <+>
 218                     text "with" <+> ppr given_eqs
 219         ; (dicts0, binds0)  <- normaliseInsts is_wanted dicts
 220         ; (dicts1, binds1)  <- substEqInDictInsts given_eqs dicts0
 221         ; let binds01 = binds0 `unionBags` binds1
 222         ; if isEmptyBag binds1
 223           then return (dicts1, binds01)
 224           else do { (dicts2, binds2) <- normaliseGivenDicts given_eqs dicts1
 225                   ; return (dicts2, binds01 `unionBags` binds2) } }
 226 \end{code}
 227
 228
 229 %************************************************************************
 230 %*                                                                      *
 231 \section{Normalisation of wanteds constraints}
 232 %*                                                                      *
 233 %************************************************************************
 234
 235 \begin{code}
 236 normaliseWanteds :: [Inst] -> TcM [Inst]
 237 normaliseWanteds insts
 238   = do { traceTc (text "normaliseWanteds <-" <+> ppr insts)
 239        ; result <- liftM fst $ rewriteToFixedPoint Nothing
 240                      [ ("(Occurs)",  noChange  $ occursCheckInsts)
 241                      , ("(ZONK)",    dontRerun $ zonkInsts)
 242                      , ("(TRIVIAL)", trivialInsts)
 243                      -- no `swapInsts'; it messes up error messages and should
 244                      -- not be necessary -=chak
 245                      , ("(DECOMP)",  decompInsts)
 246                      , ("(TOP)",     topInsts)
 247                      , ("(SUBST)",   substInsts)
 248                      , ("(UNIFY)",   unifyInsts)
 249                      ] insts
 250        ; traceTc (text "normaliseWanteds ->" <+> ppr result)
 251        ; return result
 252        }
 253 \end{code}
 254
 255
 256 %************************************************************************
 257 %*                                                                      *
 258 \section{Normalisation of givens constraints}
 259 %*                                                                      *
 260 %************************************************************************
 261
 262 \begin{code}
 263 normaliseGivens :: [Inst] -> TcM ([Inst], TcM ())
 264 normaliseGivens givens
 265  = do { traceTc (text "normaliseGivens <-" <+> ppr givens)
 266       ; (result, deSkolem) <-
 267           rewriteToFixedPoint (Just ("(SkolemOccurs)", skolemOccurs))
 268             [ ("(Occurs)",  noChange  $ occursCheckInsts)
 269             , ("(ZONK)",    dontRerun $ zonkInsts)
 270             , ("(TRIVIAL)", trivialInsts)
 271             , ("(SWAP)",    swapInsts)
 272             , ("(DECOMP)",  decompInsts)
 273             , ("(TOP)",     topInsts)
 274             , ("(SUBST)",   substInsts)
 275             ] givens
 276       ; traceTc (text "normaliseGivens ->" <+> ppr result)
 277       ; return (result, deSkolem)
 278       }
 279
 280 -- An explanation of what this does would be helpful! -=chak
 281 skolemOccurs :: PrecondRule
 282 skolemOccurs [] = return ([], return ())
 283 skolemOccurs (inst@(EqInst {}):insts)
 284         = do { (insts',actions) <- skolemOccurs insts
 285                -- check whether the current inst  co :: ty1 ~ ty2  suffers
 286                -- from the occurs check issue: F ty1 \in ty2
 287               ; let occurs = go False ty2
 288               ; if occurs
 289                   then
 290                       -- if it does generate two new coercions:
 291                       do { skolem_var <- newMetaTyVar TauTv (typeKind ty1)
 292                          ; let skolem_ty = TyVarTy skolem_var
 293                       --    ty1    :: ty1 ~ b
 294                          ; inst1 <- mkEqInst (EqPred ty1 skolem_ty) (mkGivenCo ty1)
 295                       --    sym co :: ty2 ~ b
 296                          ; inst2 <- mkEqInst (EqPred ty2 skolem_ty) (mkGivenCo $ fromACo $ mkSymCoI $ ACo $ fromGivenCo co)
 297                       -- to replace the old one
 298                       -- the corresponding action is
 299                       --    b := ty1
 300                          ; let action = writeMetaTyVar skolem_var ty1
 301                          ; return (inst1:inst2:insts', action >> actions)
 302                          }
 303                   else
 304                       return (inst:insts', actions)
 305              }
 306         where
 307                 ty1 = eqInstLeftTy inst
 308                 ty2 = eqInstRightTy inst
 309                 co  = eqInstCoercion inst
 310                 check :: Bool -> TcType -> Bool
 311                 check flag ty
 312                         = if flag && ty1 `tcEqType` ty
 313                                 then True
 314                                 else go flag ty
 315
 316                 go flag (TyConApp con tys)      = or $ map (check (isOpenSynTyCon con || flag)) tys
 317                 go flag (FunTy arg res) = or $ map (check flag) [arg,res]
 318                 go flag (AppTy fun arg)         = or $ map (check flag) [fun,arg]
 319                 go flag ty                      = False
 320 \end{code}
 321
 322
 323 %************************************************************************
 324 %*                                                                      *
 325 \section{Solving of wanted constraints with respect to a given set}
 326 %*                                                                      *
 327 %************************************************************************
 328
 329 \begin{code}
 330 solveWanteds :: [Inst]          -- givens
 331              -> [Inst]          -- wanteds
 332              -> TcM [Inst]      -- irreducible wanteds
 333 solveWanteds givens wanteds
 334   = do { traceTc $ text "solveWanteds <-" <+> ppr wanteds <+> text "with" <+>
 335                    ppr givens
 336        ; result <- liftM fst $ rewriteToFixedPoint Nothing
 337                      [ ("(Occurs)",  noChange $ occursCheckInsts)
 338                      , ("(TRIVIAL)", trivialInsts)
 339                      , ("(DECOMP)",  decompInsts)
 340                      , ("(TOP)",     topInsts)
 341                      , ("(GIVEN)",   givenInsts givens)
 342                      , ("(UNIFY)",   unifyInsts)
 343                      ] wanteds
 344        ; traceTc (text "solveWanteds ->" <+> ppr result)
 345        ; return result
 346        }
 347   where
 348     -- Use `substInst' with every given on all the wanteds.
 349     givenInsts :: [Inst] -> [Inst] -> TcM ([Inst],Bool)
 350     givenInsts []     wanteds = return (wanteds,False)
 351     givenInsts (g:gs) wanteds
 352       = do { (wanteds1, changed1) <- givenInsts gs wanteds
 353            ; (wanteds2, changed2) <- substInst g wanteds1
 354            ; return (wanteds2, changed1 || changed2)
 355            }
 356 \end{code}
 357
 358
 359 %************************************************************************
 360 %*                                                                      *
 361 \section{Normalisation rules and iterative rule application}
 362 %*                                                                      *
 363 %************************************************************************
 364
 365 We have four kinds of normalising rewrite rules:
 366
 367 (1) Normalisation rules that rewrite a set of insts and return a flag indicating
 368     whether any changes occurred during rewriting that necessitate re-running
 369     the current rule set.
 370
 371 (2) Precondition rules that rewrite a set of insts and return a monadic action
 372     that reverts the effect of preconditioning.
 373
 374 (3) Idempotent normalisation rules that never require re-running the rule set.
 375
 376 (4) Checking rule that does not alter the set of insts.
 377
 378 \begin{code}
 379 type RewriteRule     = [Inst] -> TcM ([Inst], Bool)   -- rewrite, maybe re-run
 380 type PrecondRule     = [Inst] -> TcM ([Inst], TcM ()) -- rewrite, revertable
 381 type IdemRewriteRule = [Inst] -> TcM [Inst]           -- rewrite, don't re-run
 382 type CheckRule       = [Inst] -> TcM ()               -- check
 383
 384 type NamedRule       = (String, RewriteRule)          -- rule with description
 385 type NamedPreRule    = (String, PrecondRule)          -- precond with desc
 386 \end{code}
 387
 388 Templates lifting idempotent and checking rules to full rules (which can be put
 389 into a rule set).
 390
 391 \begin{code}
 392 dontRerun :: IdemRewriteRule -> RewriteRule
 393 dontRerun rule insts = liftM addFalse $ rule insts
 394   where
 395     addFalse x = (x, False)
 396
 397 noChange :: CheckRule -> RewriteRule
 398 noChange rule insts = rule insts >> return (insts, False)
 399 \end{code}
 400
 401 The following function applies a set of rewrite rules until a fixed point is
 402 reached; i.e., none of the `RewriteRule's require re-running the rule set.
 403 Optionally, there may be a pre-conditing rule that is applied before any other
 404 rules are applied and before the rule set is re-run.
 405
 406 The result is the set of rewritten (i.e., normalised) insts and, in case of a
 407 pre-conditing rule, a monadic action that reverts the effects of
 408 pre-conditioning - specifically, this is removing introduced skolems.
 409
 410 \begin{code}
 411 rewriteToFixedPoint :: Maybe NamedPreRule   -- optional preconditioning rule
 412                     -> [NamedRule]          -- rule set
 413                     -> [Inst]               -- insts to rewrite
 414                     -> TcM ([Inst], TcM ())
 415 rewriteToFixedPoint precondRule rules insts
 416   = completeRewrite (return ()) precondRule insts
 417   where
 418     completeRewrite :: TcM () -> Maybe NamedPreRule -> [Inst]
 419                     -> TcM ([Inst], TcM ())
 420     completeRewrite dePrecond (Just (precondName, precond)) insts
 421       = do { (insts', dePrecond') <- precond insts
 422            ; traceTc $ text precondName <+> ppr insts'
 423            ; tryRules dePrecond rules insts'
 424            }
 425     completeRewrite dePrecond Nothing insts
 426       = tryRules dePrecond rules insts
 427
 428     tryRules dePrecond _                    []    = return ([]   , dePrecond)
 429     tryRules dePrecond []                   insts = return (insts, dePrecond)
 430     tryRules dePrecond ((name, rule):rules) insts
 431       = do { (insts', rerun) <- rule insts
 432            ; traceTc $ text name <+> ppr insts'
 433            ; if rerun then completeRewrite dePrecond precondRule insts'
 434                       else tryRules dePrecond rules insts'
 435            }
 436 \end{code}
 437
 438
 439 %************************************************************************
 440 %*                                                                      *
 441 \section{Different forms of Inst rewritings}
 442 %*                                                                      *
 443 %************************************************************************
 444
 445 Rewrite schemata applied by way of eq_rewrite and friends.
 446
 447 \begin{code}
 448
 449         -- (Trivial)
 450         --      g1 : t ~ t
 451         --              >-->
 452         --      g1 := t
 453         --
 454 trivialInsts ::
 455         [Inst]  ->              -- equations
 456         TcM ([Inst],Bool)       -- remaining equations, any changes?
 457 trivialInsts []
 458         = return ([],False)
 459 trivialInsts (i@(EqInst {}):is)
 460         = do { (is',changed)<- trivialInsts is
 461              ; if tcEqType ty1 ty2
 462                   then do { eitherEqInst i
 463                                 (\covar -> writeMetaTyVar covar ty1)
 464                                 (\_     -> return ())
 465                           ; return (is',True)
 466                           }
 467                   else return (i:is',changed)
 468              }
 469         where
 470            ty1 = eqInstLeftTy i
 471            ty2 = eqInstRightTy i
 472
 473 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 474 swapInsts :: [Inst] -> TcM ([Inst],Bool)
 475 -- All the inputs and outputs are equalities
 476 swapInsts insts
 477   = do { (insts', changeds) <- mapAndUnzipM swapInst insts
 478        ; return (insts', or changeds)
 479        }
 480
 481         -- (Swap)
 482         --      g1 : c ~ Fd
 483         --              >-->
 484         --      g2 : Fd ~ c
 485         --      g1 := sym g2
 486         --
 487         -- This is not all, is it?  Td ~ c is also rewritten to c ~ Td!
 488 swapInst i@(EqInst {})
 489         = go ty1 ty2
 490         where
 491               ty1 = eqInstLeftTy i
 492               ty2 = eqInstRightTy i
 493               go ty1 ty2                | Just ty1' <- tcView ty1
 494                                         = go ty1' ty2
 495               go ty1 ty2                | Just ty2' <- tcView ty2
 496                                         = go ty1 ty2'
 497               go (TyConApp tyCon _) _   | isOpenSynTyCon tyCon
 498                                         = return (i,False)
 499                 -- we should swap!
 500               go ty1 ty2@(TyConApp tyCon _)
 501                                         | isOpenSynTyCon tyCon
 502                                         = actual_swap ty1 ty2
 503               go ty1@(TyConApp _ _) ty2@(TyVarTy _)
 504                                         = actual_swap ty1 ty2
 505               go _ _                    = return (i,False)
 506
 507               actual_swap ty1 ty2 = do { wg_co <- eitherEqInst i
 508                                                           -- old_co := sym new_co
 509                                                           (\old_covar ->
 510                                                            do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty2 ty1)
 511                                                               ; let new_co = TyVarTy new_cotv
 512                                                               ; writeMetaTyVar old_covar (mkCoercion symCoercionTyCon [new_co])
 513                                                               ; return $ mkWantedCo new_cotv
 514                                                               })
 515                                                           -- new_co := sym old_co
 516                                                           (\old_co -> return $ mkGivenCo $ mkCoercion symCoercionTyCon [old_co])
 517                                              ; new_inst <- mkEqInst (EqPred ty2 ty1) wg_co
 518                                              ; return (new_inst,True)
 519                                              }
 520
 521 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 522 decompInsts :: [Inst] -> TcM ([Inst],Bool)
 523 decompInsts insts = do { (insts,bs) <- mapAndUnzipM decompInst insts
 524                        ; return (concat insts,or bs)
 525                        }
 526
 527         -- (Decomp)
 528         --      g1 : T cs ~ T ds
 529         --              >-->
 530         --      g21 : c1 ~ d1, ..., g2n : cn ~ dn
 531         --      g1 := T g2s
 532         --
 533         --  Works also for the case where T is actually an application of a
 534         --  type family constructor to a set of types, provided the
 535         --  applications on both sides of the ~ are identical;
 536         --  see also Note [OpenSynTyCon app] in TcUnify
 537         --
 538 decompInst :: Inst -> TcM ([Inst],Bool)
 539 decompInst i@(EqInst {})
 540   = go ty1 ty2
 541   where
 542     ty1 = eqInstLeftTy i
 543     ty2 = eqInstRightTy i
 544     go ty1 ty2
 545       | Just ty1' <- tcView ty1 = go ty1' ty2
 546       | Just ty2' <- tcView ty2 = go ty1 ty2'
 547
 548     go ty1@(TyConApp con1 tys1) ty2@(TyConApp con2 tys2)
 549       | con1 == con2 && identicalHead
 550       = do { cos <- eitherEqInst i
 551                       -- old_co := Con1 cos
 552                       (\old_covar ->
 553                         do { cotvs <- zipWithM (\t1 t2 ->
 554                                                 newMetaTyVar TauTv
 555                                                              (mkCoKind t1 t2))
 556                                                tys1 tys2
 557                            ; let cos = map TyVarTy cotvs
 558                            ; writeMetaTyVar old_covar (TyConApp con1 cos)
 559                            ; return $ map mkWantedCo cotvs
 560                            })
 561                       -- co_i := Con_i old_co
 562                       (\old_co -> return $
 563                                     map mkGivenCo $
 564                                         mkRightCoercions (length tys1) old_co)
 565            ; insts <- zipWithM mkEqInst (zipWith EqPred tys1 tys2) cos
 566            ; traceTc (text "decomp identicalHead" <+> ppr insts)
 567            ; return (insts, not $ null insts)
 568            }
 569       | con1 /= con2 && not (isOpenSynTyCon con1 || isOpenSynTyCon con2)
 570         -- not matching data constructors (of any flavour) are bad news
 571       = do { env0 <- tcInitTidyEnv
 572            ; let (env1, tidy_ty1) = tidyOpenType env0 ty1
 573                  (env2, tidy_ty2) = tidyOpenType env1 ty2
 574                  extra            = sep [ppr tidy_ty1, char '~', ppr tidy_ty2]
 575                  msg              =
 576                    ptext SLIT("Unsolvable equality constraint:")
 577            ; failWithTcM (env2, hang msg 2 extra)
 578            }
 579       where
 580         n                = tyConArity con1
 581         (idxTys1, tys1') = splitAt n tys1
 582         (idxTys2, tys2') = splitAt n tys2
 583         identicalHead    = not (isOpenSynTyCon con1) ||
 584                            idxTys1 `tcEqTypes` idxTys2
 585
 586     go _ _ = return ([i], False)
 587
 588 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 589 topInsts :: [Inst] -> TcM ([Inst],Bool)
 590 topInsts insts
 591         =  do { (insts,bs) <- mapAndUnzipM topInst insts
 592               ; return (insts,or bs)
 593               }
 594
 595         -- (Top)
 596         --      g1 : t ~ s
 597         --              >--> co1 :: t ~ t' / co2 :: s ~ s'
 598         --      g2 : t' ~ s'
 599         --      g1 := co1 * g2 * sym co2
 600 topInst :: Inst -> TcM (Inst,Bool)
 601 topInst i@(EqInst {})
 602         = do { (coi1,ty1') <- tcNormalizeFamInst ty1
 603              ; (coi2,ty2') <- tcNormalizeFamInst ty2
 604              ; case (coi1,coi2) of
 605                 (IdCo,IdCo) ->
 606                   return (i,False)
 607                 _           ->
 608                  do { wg_co <- eitherEqInst i
 609                                  -- old_co = co1 * new_co * sym co2
 610                                  (\old_covar ->
 611                                   do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty1 ty2)
 612                                      ; let new_co = TyVarTy new_cotv
 613                                      ; let old_coi = coi1 `mkTransCoI` ACo new_co `mkTransCoI` (mkSymCoI coi2)
 614                                      ; writeMetaTyVar old_covar (fromACo old_coi)
 615                                      ; return $ mkWantedCo new_cotv
 616                                      })
 617                                  -- new_co = sym co1 * old_co * co2
 618                                  (\old_co -> return $ mkGivenCo $ fromACo $ mkSymCoI coi1 `mkTransCoI` ACo old_co `mkTransCoI` coi2)
 619                     ; new_inst <- mkEqInst (EqPred ty1' ty2') wg_co
 620                     ; return (new_inst,True)
 621                     }
 622              }
 623         where
 624               ty1 = eqInstLeftTy i
 625               ty2 = eqInstRightTy i
 626
 627 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 628 substInsts :: [Inst] -> TcM ([Inst],Bool)
 629 substInsts insts = substInstsWorker insts []
 630
 631 substInstsWorker [] acc
 632         = return (acc,False)
 633 substInstsWorker (i:is) acc
 634         | (TyConApp con _) <- tci_left i, isOpenSynTyCon con
 635         = do { (is',change) <- substInst i (acc ++ is)
 636              ; if change
 637                   then return ((i:is'),True)
 638                   else substInstsWorker is (i:acc)
 639              }
 640         | otherwise
 641         = substInstsWorker is (i:acc)
 642
 643         -- (Subst)
 644         --      g : F c ~ t,
 645         --      forall g1 : s1{F c} ~ s2{F c}
 646         --              >-->
 647         --      g2 : s1{t} ~ s2{t}
 648         --      g1 := s1{g} * g2  * sym s2{g}           <=>     g2 := sym s1{g} * g1 * s2{g}
 649 substInst inst []
 650         = return ([],False)
 651 substInst inst@(EqInst {tci_left = pattern, tci_right = target}) (i@(EqInst {tci_left = ty1, tci_right = ty2}):is)
 652         = do { (is',changed) <- substInst inst is
 653              ; (coi1,ty1')   <- tcGenericNormalizeFamInst fun ty1
 654              ; (coi2,ty2')   <- tcGenericNormalizeFamInst fun ty2
 655              ; case (coi1,coi2) of
 656                 (IdCo,IdCo) ->
 657                   return (i:is',changed)
 658                 _           ->
 659                   do { gw_co <- eitherEqInst i
 660                                   -- old_co := co1 * new_co * sym co2
 661                                   (\old_covar ->
 662                                    do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty1' ty2')
 663                                       ; let new_co = TyVarTy new_cotv
 664                                       ; let old_coi = coi1 `mkTransCoI` ACo new_co `mkTransCoI` (mkSymCoI coi2)
 665                                       ; writeMetaTyVar old_covar (fromACo old_coi)
 666                                       ; return $ mkWantedCo new_cotv
 667                                       })
 668                                   -- new_co := sym co1 * old_co * co2
 669                                   (\old_co -> return $ mkGivenCo $ fromACo $ (mkSymCoI coi1) `mkTransCoI` ACo old_co `mkTransCoI` coi2)
 670                      ; new_inst <- mkEqInst (EqPred ty1' ty2') gw_co
 671                      ; return (new_inst:is',True)
 672                      }
 673              }
 674         where fun ty = return $ if tcEqType pattern ty then Just (target,coercion) else Nothing
 675
 676               coercion = eitherEqInst inst TyVarTy id
 677 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 678 unifyInsts
 679         :: [Inst]               -- wanted equations
 680         -> TcM ([Inst],Bool)
 681 unifyInsts insts
 682         = do { (insts',changeds) <- mapAndUnzipM unifyInst insts
 683              ; return (concat insts',or changeds)
 684              }
 685
 686         -- (UnifyMeta)
 687         --      g : alpha ~ t
 688         --              >-->
 689         --      alpha := t
 690         --      g     := t
 691         --
 692         --  TOMDO: you should only do this for certain `meta' type variables
 693 unifyInst i@(EqInst {tci_left = ty1, tci_right = ty2})
 694         | TyVarTy tv1 <- ty1, isMetaTyVar tv1   = go ty2 tv1
 695         | TyVarTy tv2 <- ty2, isMetaTyVar tv2   = go ty1 tv2
 696         | otherwise                             = return ([i],False)
 697         where go ty tv
 698                 = do { let cotv = fromWantedCo "unifyInst" $ eqInstCoercion i
 699                      ; writeMetaTyVar tv   ty   --      alpha := t
 700                      ; writeMetaTyVar cotv ty   --      g     := t
 701                      ; return ([],True)
 702                      }
 703
 704 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 705 occursCheckInsts :: [Inst] -> TcM ()
 706 occursCheckInsts insts = mappM_ occursCheckInst insts
 707
 708
 709         -- (OccursCheck)
 710         --      t ~ s[T t]
 711         --              >-->
 712         --      fail
 713         --
 714 occursCheckInst :: Inst -> TcM ()
 715 occursCheckInst i@(EqInst {tci_left = ty1, tci_right = ty2})
 716         = go ty2
 717         where
 718                 check ty = if ty `tcEqType` ty1
 719                               then occursError
 720                               else go ty
 721
 722                 go (TyConApp con tys)   = if isOpenSynTyCon con then return () else mappM_ check tys
 723                 go (FunTy arg res)      = mappM_ check [arg,res]
 724                 go (AppTy fun arg)      = mappM_ check [fun,arg]
 725                 go _                    = return ()
 726
 727                 occursError             = do { env0 <- tcInitTidyEnv
 728                                              ; let (env1, tidy_ty1)  =  tidyOpenType env0 ty1
 729                                                    (env2, tidy_ty2)  =  tidyOpenType env1 ty2
 730                                                    extra = sep [ppr tidy_ty1, char '~', ppr tidy_ty2]
 731                                              ; failWithTcM (env2, hang msg 2 extra)
 732                                              }
 733                                         where msg = ptext SLIT("Occurs check: cannot construct the infinite type")
 734 \end{code}
 735
 736 Normalises a set of dictionaries relative to a set of given equalities (which
 737 are interpreted as rewrite rules).  We only consider given equalities of the
 738 form
 739
 740   F ts ~ t
 741
 742 where F is a type family.
 743
 744 \begin{code}
 745 substEqInDictInsts :: [Inst]    -- given equalities (used as rewrite rules)
 746                    -> [Inst]    -- dictinaries to be normalised
 747                    -> TcM ([Inst], TcDictBinds)
 748 substEqInDictInsts eq_insts insts
 749   = do { traceTc (text "substEqInDictInst <-" <+> ppr insts)
 750        ; result <- foldlM rewriteWithOneEquality (insts, emptyBag) eq_insts
 751        ; traceTc (text "substEqInDictInst ->" <+> ppr result)
 752        ; return result
 753        }
 754   where
 755       -- (1) Given equality of form 'F ts ~ t': use for rewriting
 756     rewriteWithOneEquality (insts, dictBinds)
 757                            inst@(EqInst {tci_left  = pattern,
 758                                          tci_right = target})
 759       | isOpenSynTyConApp pattern
 760       = do { (insts', moreDictBinds) <- genericNormaliseInsts True {- wanted -}
 761                                                               applyThisEq insts
 762            ; return (insts', dictBinds `unionBags` moreDictBinds)
 763            }
 764       where
 765         applyThisEq = tcGenericNormalizeFamInstPred (return . matchResult)
 766
 767         -- rewrite in case of an exact match
 768         matchResult ty | tcEqType pattern ty = Just (target, eqInstType inst)
 769                        | otherwise           = Nothing
 770
 771       -- (2) Given equality has the wrong form: ignore
 772     rewriteWithOneEquality (insts, dictBinds) _not_a_rewrite_rule
 773       = return (insts, dictBinds)
 774 \end{code}
 775
 776 %************************************************************************
 777 %*                                                                      *
 778         Normalisation of Insts
 779 %*                                                                      *
 780 %************************************************************************
 781
 782 Take a bunch of Insts (not EqInsts), and normalise them wrt the top-level
 783 type-function equations, where
 784
 785         (norm_insts, binds) = normaliseInsts is_wanted insts
 786
 787 If 'is_wanted'
 788   = True,  (binds + norm_insts) defines insts       (wanteds)
 789   = False, (binds + insts)      defines norm_insts  (givens)
 790
 791 \begin{code}
 792 normaliseInsts :: Bool                          -- True <=> wanted insts
 793                -> [Inst]                        -- wanted or given insts
 794                -> TcM ([Inst], TcDictBinds)     -- normalized insts and bindings
 795 normaliseInsts isWanted insts
 796   = genericNormaliseInsts isWanted tcNormalizeFamInstPred insts
 797
 798 genericNormaliseInsts  :: Bool                      -- True <=> wanted insts
 799                        -> (TcPredType -> TcM (CoercionI, TcPredType))
 800                                                     -- how to normalise
 801                        -> [Inst]                    -- wanted or given insts
 802                        -> TcM ([Inst], TcDictBinds) -- normalized insts & binds
 803 genericNormaliseInsts isWanted fun insts
 804   = do { (insts', binds) <- mapAndUnzipM (normaliseOneInst isWanted fun) insts
 805        ; return (insts', unionManyBags binds)
 806        }
 807   where
 808     normaliseOneInst isWanted fun
 809                      dict@(Dict {tci_name = name,
 810                                  tci_pred = pred,
 811                                  tci_loc  = loc})
 812       = do { traceTc (text "genericNormaliseInst 1")
 813            ; (coi, pred') <- fun pred
 814            ; traceTc (text "genericNormaliseInst 2")
 815
 816            ; case coi of
 817                IdCo   -> return (dict, emptyBag)
 818                          -- don't use pred' in this case; otherwise, we get
 819                          -- more unfolded closed type synonyms in error messages
 820                ACo co ->
 821                  do { -- an inst for the new pred
 822                     ; dict' <- newDictBndr loc pred'
 823                       -- relate the old inst to the new one
 824                       -- target_dict = source_dict `cast` st_co
 825                     ; let (target_dict, source_dict, st_co)
 826                             | isWanted  = (dict,  dict', mkSymCoercion co)
 827                             | otherwise = (dict', dict,  co)
 828                               -- if isWanted
 829                               --        co :: dict ~ dict'
 830                               --        hence dict = dict' `cast` sym co
 831                               -- else
 832                               --        co :: dict ~ dict'
 833                               --        hence dict' = dict `cast` co
 834                           expr      = HsVar $ instToId source_dict
 835                           cast_expr = HsWrap (WpCo st_co) expr
 836                           rhs       = L (instLocSpan loc) cast_expr
 837                           binds     = mkBind target_dict rhs
 838                       -- return the new inst
 839                     ; return (dict', binds)
 840                     }
 841            }
 842
 843         -- TOMDO: treat other insts appropriately
 844     normaliseOneInst isWanted fun inst
 845       = do { inst' <- zonkInst inst
 846            ; return (inst', emptyBag)
 847            }
 848
 849 addBind binds inst rhs = binds `unionBags` mkBind inst rhs
 850
 851 mkBind inst rhs = unitBag (L (instSpan inst)
 852                           (VarBind (instToId inst) rhs))
 853 \end{code}