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