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