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