compiler/typecheck/TcTyFuns.lhs

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