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         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            ; traceTc (text "decomp identicalHead" <+> ppr insts)
 590            ; return (insts, not $ null insts)
 591            }
 592       | con1 /= con2 && not (isOpenSynTyCon con1 || isOpenSynTyCon con2)
 593         -- not matching data constructors (of any flavour) are bad news
 594       = do { env0 <- tcInitTidyEnv
 595            ; let (env1, tidy_ty1) = tidyOpenType env0 ty1
 596                  (env2, tidy_ty2) = tidyOpenType env1 ty2
 597                  extra            = sep [ppr tidy_ty1, char '~', ppr tidy_ty2]
 598                  msg              =
 599                    ptext SLIT("Unsolvable equality constraint:")
 600            ; failWithTcM (env2, hang msg 2 extra)
 601            }
 602       where
 603         n                = tyConArity con1
 604         (idxTys1, tys1') = splitAt n tys1
 605         (idxTys2, tys2') = splitAt n tys2
 606         identicalHead    = not (isOpenSynTyCon con1) ||
 607                            idxTys1 `tcEqTypes` idxTys2
 608
 609     go _ _ = return ([i], False)
 610
 611 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 612 topInsts :: [Inst] -> TcM ([Inst],Bool)
 613 topInsts insts
 614         =  do { (insts,bs) <- mapAndUnzipM topInst insts
 615               ; return (insts,or bs)
 616               }
 617
 618         -- (Top)
 619         --      g1 : t ~ s
 620         --              >--> co1 :: t ~ t' / co2 :: s ~ s'
 621         --      g2 : t' ~ s'
 622         --      g1 := co1 * g2 * sym co2
 623 topInst :: Inst -> TcM (Inst,Bool)
 624 topInst i@(EqInst {})
 625         = do { (coi1,ty1') <- tcNormalizeFamInst ty1
 626              ; (coi2,ty2') <- tcNormalizeFamInst ty2
 627              ; case (coi1,coi2) of
 628                 (IdCo,IdCo) ->
 629                   return (i,False)
 630                 _           ->
 631                  do { wg_co <- eitherEqInst i
 632                                  -- old_co = co1 * new_co * sym co2
 633                                  (\old_covar ->
 634                                   do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty1 ty2)
 635                                      ; let new_co = TyVarTy new_cotv
 636                                      ; let old_coi = coi1 `mkTransCoI` ACo new_co `mkTransCoI` (mkSymCoI coi2)
 637                                      ; writeMetaTyVar old_covar (fromACo old_coi)
 638                                      ; return $ mkWantedCo new_cotv
 639                                      })
 640                                  -- new_co = sym co1 * old_co * co2
 641                                  (\old_co -> return $ mkGivenCo $ fromACo $ mkSymCoI coi1 `mkTransCoI` ACo old_co `mkTransCoI` coi2)
 642                     ; new_inst <- mkEqInst (EqPred ty1' ty2') wg_co
 643                     ; return (new_inst,True)
 644                     }
 645              }
 646         where
 647               ty1 = eqInstLeftTy i
 648               ty2 = eqInstRightTy i
 649
 650 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 651 substInsts :: [Inst] -> TcM ([Inst],Bool)
 652 substInsts insts = substInstsWorker insts []
 653
 654 substInstsWorker [] acc
 655         = return (acc,False)
 656 substInstsWorker (i:is) acc
 657         | (TyConApp con _) <- tci_left i, isOpenSynTyCon con
 658         = do { (is',change) <- substInst i (acc ++ is)
 659              ; if change
 660                   then return ((i:is'),True)
 661                   else substInstsWorker is (i:acc)
 662              }
 663         | otherwise
 664         = substInstsWorker is (i:acc)
 665
 666         -- (Subst)
 667         --      g : F c ~ t,
 668         --      forall g1 : s1{F c} ~ s2{F c}
 669         --              >-->
 670         --      g2 : s1{t} ~ s2{t}
 671         --      g1 := s1{g} * g2  * sym s2{g}           <=>     g2 := sym s1{g} * g1 * s2{g}
 672 substInst inst []
 673         = return ([],False)
 674 substInst inst@(EqInst {tci_left = pattern, tci_right = target}) (i@(EqInst {tci_left = ty1, tci_right = ty2}):is)
 675         = do { (is',changed) <- substInst inst is
 676              ; (coi1,ty1')   <- tcGenericNormalizeFamInst fun ty1
 677              ; (coi2,ty2')   <- tcGenericNormalizeFamInst fun ty2
 678              ; case (coi1,coi2) of
 679                 (IdCo,IdCo) ->
 680                   return (i:is',changed)
 681                 _           ->
 682                   do { gw_co <- eitherEqInst i
 683                                   -- old_co := co1 * new_co * sym co2
 684                                   (\old_covar ->
 685                                    do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty1' ty2')
 686                                       ; let new_co = TyVarTy new_cotv
 687                                       ; let old_coi = coi1 `mkTransCoI` ACo new_co `mkTransCoI` (mkSymCoI coi2)
 688                                       ; writeMetaTyVar old_covar (fromACo old_coi)
 689                                       ; return $ mkWantedCo new_cotv
 690                                       })
 691                                   -- new_co := sym co1 * old_co * co2
 692                                   (\old_co -> return $ mkGivenCo $ fromACo $ (mkSymCoI coi1) `mkTransCoI` ACo old_co `mkTransCoI` coi2)
 693                      ; new_inst <- mkEqInst (EqPred ty1' ty2') gw_co
 694                      ; return (new_inst:is',True)
 695                      }
 696              }
 697         where fun ty = return $ if tcEqType pattern ty then Just (target,coercion) else Nothing
 698
 699               coercion = eitherEqInst inst TyVarTy id
 700 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 701 unifyInsts
 702         :: [Inst]               -- wanted equations
 703         -> TcM ([Inst],Bool)
 704 unifyInsts insts
 705         = do { (insts',changeds) <- mapAndUnzipM unifyInst insts
 706              ; return (concat insts',or changeds)
 707              }
 708
 709         -- (UnifyMeta)
 710         --      g : alpha ~ t
 711         --              >-->
 712         --      alpha := t
 713         --      g     := t
 714         --
 715         --  TOMDO: you should only do this for certain `meta' type variables
 716 unifyInst i@(EqInst {tci_left = ty1, tci_right = ty2})
 717         | TyVarTy tv1 <- ty1, isMetaTyVar tv1   = go ty2 tv1
 718         | TyVarTy tv2 <- ty2, isMetaTyVar tv2   = go ty1 tv2
 719         | otherwise                             = return ([i],False)
 720         where go ty tv
 721                 = do { let cotv = fromWantedCo "unifyInst" $ eqInstCoercion i
 722                      ; writeMetaTyVar tv   ty   --      alpha := t
 723                      ; writeMetaTyVar cotv ty   --      g     := t
 724                      ; return ([],True)
 725                      }
 726
 727 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 728 occursCheckInsts :: [Inst] -> TcM ()
 729 occursCheckInsts insts = mappM_ occursCheckInst insts
 730
 731
 732         -- (OccursCheck)
 733         --      t ~ s[T t]
 734         --              >-->
 735         --      fail
 736         --
 737 occursCheckInst :: Inst -> TcM ()
 738 occursCheckInst i@(EqInst {tci_left = ty1, tci_right = ty2})
 739         = go ty2
 740         where
 741                 check ty = if ty `tcEqType` ty1
 742                               then occursError
 743                               else go ty
 744
 745                 go (TyConApp con tys)   = if isOpenSynTyCon con then return () else mappM_ check tys
 746                 go (FunTy arg res)      = mappM_ check [arg,res]
 747                 go (AppTy fun arg)      = mappM_ check [fun,arg]
 748                 go _                    = return ()
 749
 750                 occursError             = do { env0 <- tcInitTidyEnv
 751                                              ; let (env1, tidy_ty1)  =  tidyOpenType env0 ty1
 752                                                    (env2, tidy_ty2)  =  tidyOpenType env1 ty2
 753                                                    extra = sep [ppr tidy_ty1, char '~', ppr tidy_ty2]
 754                                              ; failWithTcM (env2, hang msg 2 extra)
 755                                              }
 756                                         where msg = ptext SLIT("Occurs check: cannot construct the infinite type")
 757 \end{code}
 758
 759 Normalises a set of dictionaries relative to a set of given equalities (which
 760 are interpreted as rewrite rules).  We only consider given equalities of the
 761 form
 762
 763   F ts ~ t
 764
 765 where F is a type family.
 766
 767 \begin{code}
 768 substEqInDictInsts :: [Inst]    -- given equalities (used as rewrite rules)
 769                    -> [Inst]    -- dictinaries to be normalised
 770                    -> TcM ([Inst], TcDictBinds)
 771 substEqInDictInsts eq_insts insts
 772   = do { traceTc (text "substEqInDictInst <-" <+> ppr insts)
 773        ; result <- foldlM rewriteWithOneEquality (insts, emptyBag) eq_insts
 774        ; traceTc (text "substEqInDictInst ->" <+> ppr result)
 775        ; return result
 776        }
 777   where
 778       -- (1) Given equality of form 'F ts ~ t': use for rewriting
 779     rewriteWithOneEquality (insts, dictBinds)
 780                            inst@(EqInst {tci_left  = pattern,
 781                                          tci_right = target})
 782       | isOpenSynTyConApp pattern
 783       = do { (insts', moreDictBinds) <- genericNormaliseInsts True {- wanted -}
 784                                                               applyThisEq insts
 785            ; return (insts', dictBinds `unionBags` moreDictBinds)
 786            }
 787       where
 788         applyThisEq = tcGenericNormalizeFamInstPred (return . matchResult)
 789
 790         -- rewrite in case of an exact match
 791         matchResult ty | tcEqType pattern ty = Just (target, eqInstType inst)
 792                        | otherwise           = Nothing
 793
 794       -- (2) Given equality has the wrong form: ignore
 795     rewriteWithOneEquality (insts, dictBinds) _not_a_rewrite_rule
 796       = return (insts, dictBinds)
 797 \end{code}
 798
 799 %************************************************************************
 800 %*                                                                      *
 801         Normalisation of Insts
 802 %*                                                                      *
 803 %************************************************************************
 804
 805 Take a bunch of Insts (not EqInsts), and normalise them wrt the top-level
 806 type-function equations, where
 807
 808         (norm_insts, binds) = normaliseInsts is_wanted insts
 809
 810 If 'is_wanted'
 811   = True,  (binds + norm_insts) defines insts       (wanteds)
 812   = False, (binds + insts)      defines norm_insts  (givens)
 813
 814 \begin{code}
 815 normaliseInsts :: Bool                          -- True <=> wanted insts
 816                -> [Inst]                        -- wanted or given insts
 817                -> TcM ([Inst], TcDictBinds)     -- normalized insts and bindings
 818 normaliseInsts isWanted insts
 819   = genericNormaliseInsts isWanted tcNormalizeFamInstPred insts
 820
 821 genericNormaliseInsts  :: Bool                      -- True <=> wanted insts
 822                        -> (TcPredType -> TcM (CoercionI, TcPredType))
 823                                                     -- how to normalise
 824                        -> [Inst]                    -- wanted or given insts
 825                        -> TcM ([Inst], TcDictBinds) -- normalized insts & binds
 826 genericNormaliseInsts isWanted fun insts
 827   = do { (insts', binds) <- mapAndUnzipM (normaliseOneInst isWanted fun) insts
 828        ; return (insts', unionManyBags binds)
 829        }
 830   where
 831     normaliseOneInst isWanted fun
 832                      dict@(Dict {tci_name = name,
 833                                  tci_pred = pred,
 834                                  tci_loc  = loc})
 835       = do { traceTc (text "genericNormaliseInst 1")
 836            ; (coi, pred') <- fun pred
 837            ; traceTc (text "genericNormaliseInst 2")
 838
 839            ; case coi of
 840                IdCo   -> return (dict, emptyBag)
 841                          -- don't use pred' in this case; otherwise, we get
 842                          -- more unfolded closed type synonyms in error messages
 843                ACo co ->
 844                  do { -- an inst for the new pred
 845                     ; dict' <- newDictBndr loc pred'
 846                       -- relate the old inst to the new one
 847                       -- target_dict = source_dict `cast` st_co
 848                     ; let (target_dict, source_dict, st_co)
 849                             | isWanted  = (dict,  dict', mkSymCoercion co)
 850                             | otherwise = (dict', dict,  co)
 851                               -- if isWanted
 852                               --        co :: dict ~ dict'
 853                               --        hence dict = dict' `cast` sym co
 854                               -- else
 855                               --        co :: dict ~ dict'
 856                               --        hence dict' = dict `cast` co
 857                           expr      = HsVar $ instToId source_dict
 858                           cast_expr = HsWrap (WpCo st_co) expr
 859                           rhs       = L (instLocSpan loc) cast_expr
 860                           binds     = mkBind target_dict rhs
 861                       -- return the new inst
 862                     ; return (dict', binds)
 863                     }
 864            }
 865
 866         -- TOMDO: treat other insts appropriately
 867     normaliseOneInst isWanted fun inst
 868       = do { inst' <- zonkInst inst
 869            ; return (inst', emptyBag)
 870            }
 871
 872 addBind binds inst rhs = binds `unionBags` mkBind inst rhs
 873
 874 mkBind inst rhs = unitBag (L (instSpan inst)
 875                           (VarBind (instToId inst) rhs))
 876 \end{code}