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