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