compiler/typecheck/TcTyFuns.lhs

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