compiler/typecheck/TcGadt.lhs

   1 %
   2 % (c) The University of Glasgow 2006
   3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   4 %
   5
   6 %************************************************************************
   7 %*                                                                      *
   8                 Type refinement for GADTs
   9 %*                                                                      *
  10 %************************************************************************
  11
  12 \begin{code}
  13 module TcGadt (
  14         Refinement, emptyRefinement, isEmptyRefinement,
  15         gadtRefine,
  16         refineType, refinePred, refineResType,
  17         tcUnifyTys, BindFlag(..)
  18   ) where
  19
  20 #include "HsVersions.h"
  21
  22 import HsSyn
  23 import Coercion
  24 import Type
  25
  26 import TypeRep
  27 import Var
  28 import VarEnv
  29 import VarSet
  30 import ErrUtils
  31 import Maybes
  32 import Control.Monad
  33 import Outputable
  34 import TcType
  35
  36 #ifdef DEBUG
  37 import Unique
  38 import UniqFM
  39 #endif
  40 \end{code}
  41
  42
  43 %************************************************************************
  44 %*                                                                      *
  45                 What a refinement is
  46 %*                                                                      *
  47 %************************************************************************
  48
  49 \begin{code}
  50 data Refinement = Reft InScopeSet InternalReft
  51
  52 type InternalReft = TyVarEnv (Coercion, Type)
  53 -- INVARIANT:   a->(co,ty)   then   co :: (a:=:ty)
  54 -- Not necessarily idemopotent
  55
  56 instance Outputable Refinement where
  57   ppr (Reft in_scope env)
  58     = ptext SLIT("Refinement") <+>
  59         braces (ppr env)
  60
  61 emptyRefinement :: Refinement
  62 emptyRefinement = (Reft emptyInScopeSet emptyVarEnv)
  63
  64 isEmptyRefinement :: Refinement -> Bool
  65 isEmptyRefinement (Reft _ env) = isEmptyVarEnv env
  66
  67 refineType :: Refinement -> Type -> Maybe (Coercion, Type)
  68 -- Apply the refinement to the type.
  69 -- If (refineType r ty) = (co, ty')
  70 -- Then co :: ty:=:ty'
  71 -- Nothing => the refinement does nothing to this type
  72 refineType (Reft in_scope env) ty
  73   | not (isEmptyVarEnv env),            -- Common case
  74     any (`elemVarEnv` env) (varSetElems (tyVarsOfType ty))
  75   = Just (substTy co_subst ty, substTy tv_subst ty)
  76   | otherwise
  77   = Nothing     -- The type doesn't mention any refined type variables
  78   where
  79     tv_subst = mkTvSubst in_scope (mapVarEnv snd env)
  80     co_subst = mkTvSubst in_scope (mapVarEnv fst env)
  81
  82 refinePred :: Refinement -> PredType -> Maybe (Coercion, PredType)
  83 refinePred (Reft in_scope env) pred
  84   | not (isEmptyVarEnv env),            -- Common case
  85     any (`elemVarEnv` env) (varSetElems (tyVarsOfPred pred))
  86   = Just (mkPredTy (substPred co_subst pred), substPred tv_subst pred)
  87   | otherwise
  88   = Nothing     -- The type doesn't mention any refined type variables
  89   where
  90     tv_subst = mkTvSubst in_scope (mapVarEnv snd env)
  91     co_subst = mkTvSubst in_scope (mapVarEnv fst env)
  92
  93 refineResType :: Refinement -> Type -> (HsWrapper, Type)
  94 -- Like refineType, but returns the 'sym' coercion
  95 -- If (refineResType r ty) = (co, ty')
  96 -- Then co :: ty':=:ty
  97 -- It's convenient to return a HsWrapper here
  98 refineResType reft ty
  99   = case refineType reft ty of
 100         Just (co, ty1) -> (WpCo (mkSymCoercion co), ty1)
 101         Nothing        -> (idHsWrapper,             ty)
 102 \end{code}
 103
 104
 105 %************************************************************************
 106 %*                                                                      *
 107                 Generating a type refinement
 108 %*                                                                      *
 109 %************************************************************************
 110
 111 \begin{code}
 112 gadtRefine :: Refinement
 113            -> [TyVar]   -- Bind these by preference
 114            -> [CoVar]
 115            -> MaybeErr Message Refinement
 116 \end{code}
 117
 118 (gadtRefine cvs) takes a list of coercion variables, and returns a
 119 list of coercions, obtained by unifying the types equated by the
 120 incoming coercions.  The returned coercions all have kinds of form
 121 (a:=:ty), where a is a rigid type variable.
 122
 123 Example:
 124   gadtRefine [c :: (a,Int):=:(Bool,b)]
 125   = [ right (left c) :: a:=:Bool,
 126       sym (right c)  :: b:=:Int ]
 127
 128 That is, given evidence 'c' that (a,Int)=(Bool,b), it returns derived
 129 evidence in easy-to-use form.  In particular, given any e::ty, we know
 130 that:
 131         e `cast` ty[right (left c)/a, sym (right c)/b]
 132         :: ty [Bool/a, Int/b]
 133
 134 Two refinements:
 135
 136 - It can fail, if the coercion is unsatisfiable.
 137
 138 - It's biased, by being given a set of type variables to bind
 139   when there is a choice. Example:
 140         MkT :: forall a. a -> T [a]
 141         f :: forall b. T [b] -> b
 142         f x = let v = case x of { MkT y -> y }
 143               in ...
 144   Here we want to bind [a->b], not the other way round, because
 145   in this example the return type is wobbly, and we want the
 146   program to typecheck
 147
 148
 149 -- E.g. (a, Bool, right (left c))
 150 -- INVARIANT: in the triple (tv, ty, co), we have (co :: tv:=:ty)
 151 -- The result is idempotent: the
 152
 153 \begin{code}
 154 gadtRefine (Reft in_scope env1)
 155            ex_tvs co_vars
 156 -- Precondition: fvs( co_vars ) # env1
 157 -- That is, the kinds of the co_vars are a
 158 -- fixed point of the incoming refinement
 159
 160   = ASSERT2( not $ any (`elemVarEnv` env1) (varSetElems $ tyVarsOfTypes $ map tyVarKind co_vars),
 161              ppr env1 $$ ppr co_vars $$ ppr (map tyVarKind co_vars) )
 162     initUM (tryToBind tv_set) $
 163     do  {       -- Run the unifier, starting with an empty env
 164         ; env2 <- foldM do_one emptyInternalReft co_vars
 165
 166                 -- Find the fixed point of the resulting
 167                 -- non-idempotent substitution
 168         ; let tmp_env = env1 `plusVarEnv` env2
 169               out_env = fixTvCoEnv in_scope' tmp_env
 170         ; WARN( not (null (badReftElts tmp_env)), ppr (badReftElts tmp_env) $$ ppr tmp_env )
 171           WARN( not (null (badReftElts out_env)), ppr (badReftElts out_env) $$ ppr out_env )
 172           return (Reft in_scope' out_env) }
 173   where
 174     tv_set = mkVarSet ex_tvs
 175     in_scope' = foldr extend in_scope co_vars
 176
 177         -- For each co_var, add it *and* the tyvars it mentions, to in_scope
 178     extend co_var in_scope
 179         = extendInScopeSetSet in_scope $
 180           extendVarSet (tyVarsOfType (tyVarKind co_var)) co_var
 181
 182     do_one reft co_var = unify reft (TyVarTy co_var) ty1 ty2
 183         where
 184            (ty1,ty2) = splitCoercionKind (tyVarKind co_var)
 185 \end{code}
 186
 187 %************************************************************************
 188 %*                                                                      *
 189                 Unification
 190 %*                                                                      *
 191 %************************************************************************
 192
 193 \begin{code}
 194 tcUnifyTys :: (TyVar -> BindFlag)
 195            -> [Type] -> [Type]
 196            -> Maybe TvSubst     -- A regular one-shot substitution
 197 -- The two types may have common type variables, and indeed do so in the
 198 -- second call to tcUnifyTys in FunDeps.checkClsFD
 199 --
 200 -- We implement tcUnifyTys using the evidence-generating 'unify' function
 201 -- in this module, even though we don't need to generate any evidence.
 202 -- This is simply to avoid replicating all all the code for unify
 203 tcUnifyTys bind_fn tys1 tys2
 204   = maybeErrToMaybe $ initUM bind_fn $
 205     do { reft <- unifyList emptyInternalReft cos tys1 tys2
 206
 207         -- Find the fixed point of the resulting non-idempotent substitution
 208         ; let in_scope = mkInScopeSet (tvs1 `unionVarSet` tvs2)
 209               tv_env   = fixTvSubstEnv in_scope (mapVarEnv snd reft)
 210
 211         ; return (mkTvSubst in_scope tv_env) }
 212   where
 213     tvs1 = tyVarsOfTypes tys1
 214     tvs2 = tyVarsOfTypes tys2
 215     cos  = zipWith mkUnsafeCoercion tys1 tys2
 216
 217
 218 ----------------------------
 219 fixTvCoEnv :: InScopeSet -> InternalReft -> InternalReft
 220         -- Find the fixed point of a Refinement
 221         -- (assuming it has no loops!)
 222 fixTvCoEnv in_scope env
 223   = fixpt
 224   where
 225     fixpt         = mapVarEnv step env
 226
 227     step (co, ty) = case refineType (Reft in_scope fixpt) ty of
 228                         Nothing         -> (co,                     ty)
 229                         Just (co', ty') -> (mkTransCoercion co co', ty')
 230       -- Apply fixpt one step:
 231       -- Use refineType to get a substituted type, ty', and a coercion, co_fn,
 232       -- which justifies the substitution.  If the coercion is not the identity
 233       -- then use transitivity with the original coercion
 234
 235 -----------------------------
 236 fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv
 237 fixTvSubstEnv in_scope env
 238   = fixpt
 239   where
 240     fixpt = mapVarEnv (substTy (mkTvSubst in_scope fixpt)) env
 241
 242 ----------------------------
 243 tryToBind :: TyVarSet -> TyVar -> BindFlag
 244 tryToBind tv_set tv | tv `elemVarSet` tv_set = BindMe
 245                     | otherwise              = AvoidMe
 246
 247 \end{code}
 248
 249
 250 %************************************************************************
 251 %*                                                                      *
 252                 The workhorse
 253 %*                                                                      *
 254 %************************************************************************
 255
 256 \begin{code}
 257 #ifdef DEBUG
 258 badReftElts :: InternalReft -> [(Unique, (Coercion,Type))]
 259 -- Return the BAD elements of the refinement
 260 -- Should be empty; used in asserions only
 261 badReftElts env
 262   = filter (not . ok) (ufmToList env)
 263   where
 264     ok :: (Unique, (Coercion, Type)) -> Bool
 265     ok (u, (co, ty)) | Just tv <- tcGetTyVar_maybe ty1
 266                      = varUnique tv == u && ty `tcEqType` ty2
 267                      | otherwise = False
 268         where
 269           (ty1,ty2) = coercionKind co
 270 #endif
 271
 272 emptyInternalReft :: InternalReft
 273 emptyInternalReft = emptyVarEnv
 274
 275 unify :: InternalReft           -- An existing substitution to extend
 276       -> Coercion       -- Witness of their equality
 277       -> Type -> Type   -- Types to be unified, and witness of their equality
 278       -> UM InternalReft                -- Just the extended substitution,
 279                                 -- Nothing if unification failed
 280 -- We do not require the incoming substitution to be idempotent,
 281 -- nor guarantee that the outgoing one is.  That's fixed up by
 282 -- the wrappers.
 283
 284 -- PRE-CONDITION: in the call (unify r co ty1 ty2), we know that
 285 --                      co :: (ty1:=:ty2)
 286
 287 -- Respects newtypes, PredTypes
 288
 289 unify subst co ty1 ty2 = -- pprTrace "unify" (ppr subst <+> pprParendType ty1 <+> pprParendType ty2) $
 290                          unify_ subst co ty1 ty2
 291
 292 -- in unify_, any NewTcApps/Preds should be taken at face value
 293 unify_ subst co (TyVarTy tv1) ty2  = uVar False subst co tv1 ty2
 294 unify_ subst co ty1 (TyVarTy tv2)  = uVar True  subst co tv2 ty1
 295
 296 unify_ subst co ty1 ty2 | Just ty1' <- tcView ty1 = unify subst co ty1' ty2
 297 unify_ subst co ty1 ty2 | Just ty2' <- tcView ty2 = unify subst co ty1 ty2'
 298
 299 unify_ subst co (PredTy p1) (PredTy p2) = unify_pred subst co p1 p2
 300
 301 unify_ subst co t1@(TyConApp tyc1 tys1) t2@(TyConApp tyc2 tys2)
 302   | tyc1 == tyc2 = unify_tys subst co tys1 tys2
 303
 304 unify_ subst co (FunTy ty1a ty1b) (FunTy ty2a ty2b)
 305   = do  { let [co1,co2] = decomposeCo 2 co
 306         ; subst' <- unify subst co1 ty1a ty2a
 307         ; unify subst' co2 ty1b ty2b }
 308
 309         -- Applications need a bit of care!
 310         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
 311         -- NB: we've already dealt with type variables and Notes,
 312         -- so if one type is an App the other one jolly well better be too
 313 unify_ subst co (AppTy ty1a ty1b) ty2
 314   | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
 315   = do  { subst' <- unify subst (mkLeftCoercion co) ty1a ty2a
 316         ; unify subst' (mkRightCoercion co) ty1b ty2b }
 317
 318 unify_ subst co ty1 (AppTy ty2a ty2b)
 319   | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
 320   = do  { subst' <- unify subst (mkLeftCoercion co) ty1a ty2a
 321         ; unify subst' (mkRightCoercion co) ty1b ty2b }
 322
 323 unify_ subst co ty1 ty2 = failWith (misMatch ty1 ty2)
 324         -- ForAlls??
 325
 326
 327 ------------------------------
 328 unify_pred subst co (ClassP c1 tys1) (ClassP c2 tys2)
 329   | c1 == c2 = unify_tys subst co tys1 tys2
 330 unify_pred subst co (IParam n1 t1) (IParam n2 t2)
 331   | n1 == n2 = unify subst co t1 t2
 332 unify_pred subst co p1 p2 = failWith (misMatch (PredTy p1) (PredTy p2))
 333
 334 ------------------------------
 335 unify_tys :: InternalReft -> Coercion -> [Type] -> [Type] -> UM InternalReft
 336 unify_tys subst co xs ys
 337   = unifyList subst (decomposeCo (length xs) co) xs ys
 338
 339 unifyList :: InternalReft -> [Coercion] -> [Type] -> [Type] -> UM InternalReft
 340 unifyList subst orig_cos orig_xs orig_ys
 341   = go subst orig_cos orig_xs orig_ys
 342   where
 343     go subst _        []     []     = return subst
 344     go subst (co:cos) (x:xs) (y:ys) = do { subst' <- unify subst co x y
 345                                          ; go subst' cos xs ys }
 346     go subst _ _ _ = failWith (lengthMisMatch orig_xs orig_ys)
 347
 348 ---------------------------------
 349 uVar :: Bool            -- Swapped
 350      -> InternalReft    -- An existing substitution to extend
 351      -> Coercion
 352      -> TyVar           -- Type variable to be unified
 353      -> Type            -- with this type
 354      -> UM InternalReft
 355
 356 -- PRE-CONDITION: in the call (uVar swap r co tv1 ty), we know that
 357 --      if swap=False   co :: (tv1:=:ty)
 358 --      if swap=True    co :: (ty:=:tv1)
 359
 360 uVar swap subst co tv1 ty
 361  = -- Check to see whether tv1 is refined by the substitution
 362    case (lookupVarEnv subst tv1) of
 363
 364      -- Yes, call back into unify'
 365      Just (co',ty')     -- co' :: (tv1:=:ty')
 366         | swap          -- co :: (ty:=:tv1)
 367         -> unify subst (mkTransCoercion co co') ty ty'
 368         | otherwise     -- co :: (tv1:=:ty)
 369         -> unify subst (mkTransCoercion (mkSymCoercion co') co) ty' ty
 370
 371      -- No, continue
 372      Nothing -> uUnrefined swap subst co
 373                            tv1 ty ty
 374
 375
 376 uUnrefined :: Bool                -- Whether the input is swapped
 377            -> InternalReft        -- An existing substitution to extend
 378            -> Coercion
 379            -> TyVar               -- Type variable to be unified
 380            -> Type                -- with this type
 381            -> Type                -- (de-noted version)
 382            -> UM InternalReft
 383
 384 -- We know that tv1 isn't refined
 385 -- PRE-CONDITION: in the call (uUnrefined False r co tv1 ty2 ty2'), we know that
 386 --      co :: tv1:=:ty2
 387 -- and if the first argument is True instead, we know
 388 --      co :: ty2:=:tv1
 389
 390 uUnrefined swap subst co tv1 ty2 ty2'
 391   | Just ty2'' <- tcView ty2'
 392   = uUnrefined swap subst co tv1 ty2 ty2''      -- Unwrap synonyms
 393                 -- This is essential, in case we have
 394                 --      type Foo a = a
 395                 -- and then unify a :=: Foo a
 396
 397 uUnrefined swap subst co tv1 ty2 (TyVarTy tv2)
 398   | tv1 == tv2          -- Same type variable
 399   = return subst
 400
 401     -- Check to see whether tv2 is refined
 402   | Just (co',ty') <- lookupVarEnv subst tv2    -- co' :: tv2:=:ty'
 403   = uUnrefined False subst (mkTransCoercion (doSwap swap co) co') tv1 ty' ty'
 404
 405   -- So both are unrefined; next, see if the kinds force the direction
 406   | eqKind k1 k2        -- Can update either; so check the bind-flags
 407   = do  { b1 <- tvBindFlag tv1
 408         ; b2 <- tvBindFlag tv2
 409         ; case (b1,b2) of
 410             (BindMe, _)          -> bind swap tv1 ty2
 411
 412             (AvoidMe, BindMe)    -> bind (not swap) tv2 ty1
 413             (AvoidMe, _)         -> bind swap tv1 ty2
 414
 415             (WildCard, WildCard) -> return subst
 416             (WildCard, Skolem)   -> return subst
 417             (WildCard, _)        -> bind (not swap) tv2 ty1
 418
 419             (Skolem, WildCard)   -> return subst
 420             (Skolem, Skolem)     -> failWith (misMatch ty1 ty2)
 421             (Skolem, _)          -> bind (not swap) tv2 ty1
 422         }
 423
 424   | k1 `isSubKind` k2 = bindTv (not swap) subst co tv2 ty1  -- Must update tv2
 425   | k2 `isSubKind` k1 = bindTv swap subst co tv1 ty2        -- Must update tv1
 426
 427   | otherwise = failWith (kindMisMatch tv1 ty2)
 428   where
 429     ty1 = TyVarTy tv1
 430     k1 = tyVarKind tv1
 431     k2 = tyVarKind tv2
 432     bind swap tv ty = extendReft swap subst tv co ty
 433
 434 uUnrefined swap subst co tv1 ty2 ty2'   -- ty2 is not a type variable
 435   | tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2')
 436   = failWith (occursCheck tv1 ty2)      -- Occurs check
 437   | not (k2 `isSubKind` k1)
 438   = failWith (kindMisMatch tv1 ty2)     -- Kind check
 439   | otherwise
 440   = bindTv swap subst co tv1 ty2                -- Bind tyvar to the synonym if poss
 441   where
 442     k1 = tyVarKind tv1
 443     k2 = typeKind ty2'
 444
 445 substTvSet :: InternalReft -> TyVarSet -> TyVarSet
 446 -- Apply the non-idempotent substitution to a set of type variables,
 447 -- remembering that the substitution isn't necessarily idempotent
 448 substTvSet subst tvs
 449   = foldVarSet (unionVarSet . get) emptyVarSet tvs
 450   where
 451     get tv = case lookupVarEnv subst tv of
 452                 Nothing     -> unitVarSet tv
 453                 Just (_,ty) -> substTvSet subst (tyVarsOfType ty)
 454
 455 bindTv swap subst co tv ty      -- ty is not a type variable
 456   = do  { b <- tvBindFlag tv
 457         ; case b of
 458             Skolem   -> failWith (misMatch (TyVarTy tv) ty)
 459             WildCard -> return subst
 460             other    -> extendReft swap subst tv co ty
 461         }
 462
 463 doSwap :: Bool -> Coercion -> Coercion
 464 doSwap swap co = if swap then mkSymCoercion co else co
 465
 466 extendReft :: Bool
 467            -> InternalReft
 468            -> TyVar
 469            -> Coercion
 470            -> Type
 471            -> UM InternalReft
 472 extendReft swap subst tv  co ty
 473   = ASSERT2( (coercionKindPredTy co1 `tcEqType` mkCoKind (mkTyVarTy tv) ty),
 474           (text "Refinement invariant failure: co = " <+> ppr co1  <+> ppr (coercionKindPredTy co1) $$ text "subst = " <+> ppr tv <+> ppr (mkCoKind (mkTyVarTy tv) ty)) )
 475     return (extendVarEnv subst tv (co1, ty))
 476   where
 477     co1 = doSwap swap co
 478
 479 \end{code}
 480
 481 %************************************************************************
 482 %*                                                                      *
 483                 Unification monad
 484 %*                                                                      *
 485 %************************************************************************
 486
 487 \begin{code}
 488 data BindFlag
 489   = BindMe      -- A regular type variable
 490   | AvoidMe     -- Like BindMe but, given the choice, avoid binding it
 491
 492   | Skolem      -- This type variable is a skolem constant
 493                 -- Don't bind it; it only matches itself
 494
 495   | WildCard    -- This type variable matches anything,
 496                 -- and does not affect the substitution
 497
 498 newtype UM a = UM { unUM :: (TyVar -> BindFlag)
 499                          -> MaybeErr Message a }
 500
 501 instance Monad UM where
 502   return a = UM (\tvs -> Succeeded a)
 503   fail s   = UM (\tvs -> Failed (text s))
 504   m >>= k  = UM (\tvs -> case unUM m tvs of
 505                            Failed err -> Failed err
 506                            Succeeded v  -> unUM (k v) tvs)
 507
 508 initUM :: (TyVar -> BindFlag) -> UM a -> MaybeErr Message a
 509 initUM badtvs um = unUM um badtvs
 510
 511 tvBindFlag :: TyVar -> UM BindFlag
 512 tvBindFlag tv = UM (\tv_fn -> Succeeded (tv_fn tv))
 513
 514 failWith :: Message -> UM a
 515 failWith msg = UM (\tv_fn -> Failed msg)
 516
 517 maybeErrToMaybe :: MaybeErr fail succ -> Maybe succ
 518 maybeErrToMaybe (Succeeded a) = Just a
 519 maybeErrToMaybe (Failed m)    = Nothing
 520 \end{code}
 521
 522
 523 %************************************************************************
 524 %*                                                                      *
 525                 Error reporting
 526         We go to a lot more trouble to tidy the types
 527         in TcUnify.  Maybe we'll end up having to do that
 528         here too, but I'll leave it for now.
 529 %*                                                                      *
 530 %************************************************************************
 531
 532 \begin{code}
 533 misMatch t1 t2
 534   = ptext SLIT("Can't match types") <+> quotes (ppr t1) <+>
 535     ptext SLIT("and") <+> quotes (ppr t2)
 536
 537 lengthMisMatch tys1 tys2
 538   = sep [ptext SLIT("Can't match unequal length lists"),
 539          nest 2 (ppr tys1), nest 2 (ppr tys2) ]
 540
 541 kindMisMatch tv1 t2
 542   = vcat [ptext SLIT("Can't match kinds") <+> quotes (ppr (tyVarKind tv1)) <+>
 543             ptext SLIT("and") <+> quotes (ppr (typeKind t2)),
 544           ptext SLIT("when matching") <+> quotes (ppr tv1) <+>
 545                 ptext SLIT("with") <+> quotes (ppr t2)]
 546
 547 occursCheck tv ty
 548   = hang (ptext SLIT("Can't construct the infinite type"))
 549        2 (ppr tv <+> equals <+> ppr ty)
 550 \end{code}