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