compiler/typecheck/TcGadt.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   3 %
   4
   5 %************************************************************************
   6 %*                                                                      *
   7                 Type refinement for GADTs
   8 %*                                                                      *
   9 %************************************************************************
  10
  11 \begin{code}
  12 module TcGadt (
  13         Refinement, emptyRefinement, gadtRefine,
  14         refineType, refineResType,
  15         dataConCanMatch,
  16         tcUnifyTys, BindFlag(..)
  17   ) where
  18
  19 import HsSyn    ( ExprCoFn(..), idCoercion, isIdCoercion )
  20 import Coercion ( Coercion, mkSymCoercion, mkTransCoercion, mkUnsafeCoercion,
  21                   mkLeftCoercion, mkRightCoercion,
  22                   splitCoercionKind, decomposeCo )
  23 import TcType   ( TvSubst(..), TvSubstEnv, substTy, mkTvSubst,
  24                   substTyVar, zipTopTvSubst, typeKind,
  25                   eqKind, isSubKind, repSplitAppTy_maybe,
  26                   tcView
  27                 )
  28 import Type     ( Type, tyVarsOfType, tyVarsOfTypes )
  29 import TypeRep  ( Type(..), PredType(..) )
  30 import DataCon  ( DataCon, dataConUnivTyVars, dataConEqSpec )
  31 import Var      ( CoVar, TyVar, tyVarKind )
  32 import VarEnv
  33 import VarSet
  34 import ErrUtils         ( Message )
  35 import Maybes           ( MaybeErr(..), isJust )
  36 import Control.Monad    ( foldM )
  37 import Outputable
  38
  39 #include "HsVersions.h"
  40 \end{code}
  41
  42
  43 %************************************************************************
  44 %*                                                                      *
  45                 What a refinement is
  46 %*                                                                      *
  47 %************************************************************************
  48
  49 \begin{code}
  50 data Refinement = Reft InScopeSet TvSubstEnv CoSubstEnv
  51 type CoSubstEnv = TvSubstEnv    -- Maps type variables to *coercions*
  52 -- INVARIANT: in the refinement (tsub, csub)
  53 --            forall a. (csub(a) :: a:=:tsub(a))
  54
  55 instance Outputable Refinement where
  56   ppr (Reft in_scope tv_env co_env)
  57     = ptext SLIT("Refinment") <+>
  58         braces (ppr tv_env $$ ppr co_env)
  59
  60 emptyRefinement :: Refinement
  61 emptyRefinement = Reft emptyInScopeSet emptyVarEnv emptyVarEnv
  62
  63 refineType :: Refinement -> Type -> (ExprCoFn, 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 tv_env co_env) ty
  68   | not (isEmptyVarEnv tv_env),         -- Common case
  69     any (`elemVarEnv` tv_env) (varSetElems (tyVarsOfType ty))
  70   = (ExprCoFn (substTy co_subst ty), substTy tv_subst ty)
  71   | otherwise
  72   = (idCoercion, ty)    -- The type doesn't mention any refined type variables
  73   where
  74     tv_subst = mkTvSubst in_scope tv_env
  75     co_subst = mkTvSubst in_scope co_env
  76
  77 refineResType :: Refinement -> Type -> (ExprCoFn, 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         (ExprCoFn co, ty1) -> (ExprCoFn (mkSymCoercion co), ty1)
  84         (id_co,       ty1) -> ASSERT( isIdCoercion id_co )
  85                               (idCoercion, 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 tv_env1 co_env1)
 139            ex_tvs co_vars
 140 -- Precondition: fvs( co_vars ) # tv_env1
 141 -- That is, the kinds of the co_vars are a
 142 -- fixed point of the  incoming refinement
 143
 144   = initUM (tryToBind tv_set) $
 145     do  {       -- Run the unifier, starting with an empty env
 146         ; env2 <- foldM do_one emptyInternalReft co_vars
 147
 148                 -- Find the fixed point of the resulting
 149                 -- non-idempotent substitution
 150         ; let tv_env2 = tv_env1 `plusVarEnv` mapVarEnv snd env2
 151               co_env2 = co_env1 `plusVarEnv` mapVarEnv fst env2
 152
 153         ; return (Reft in_scope' (fixTvSubstEnv in_scope' tv_env2)
 154                                  (fixTvSubstEnv in_scope' co_env2)) }
 155   where
 156     tv_set = mkVarSet ex_tvs
 157     in_scope' = foldr extend in_scope co_vars
 158     extend co_var in_scope
 159         = extendInScopeSetSet (extendInScopeSet in_scope co_var)
 160                               (tyVarsOfType (tyVarKind co_var))
 161
 162     do_one reft co_var = unify reft (TyVarTy co_var) ty1 ty2
 163         where
 164            (ty1,ty2) = splitCoercionKind (tyVarKind co_var)
 165 \end{code}
 166
 167 %************************************************************************
 168 %*                                                                      *
 169                 Unification
 170 %*                                                                      *
 171 %************************************************************************
 172
 173 \begin{code}
 174 tcUnifyTys :: (TyVar -> BindFlag)
 175            -> [Type] -> [Type]
 176            -> Maybe TvSubst     -- A regular one-shot substitution
 177 -- The two types may have common type variables, and indeed do so in the
 178 -- second call to tcUnifyTys in FunDeps.checkClsFD
 179 --
 180 -- We implement tcUnifyTys using the evidence-generating 'unify' function
 181 -- in this module, even though we don't need to generate any evidence.
 182 -- This is simply to avoid replicating all all the code for unify
 183 tcUnifyTys bind_fn tys1 tys2
 184   = maybeErrToMaybe $ initUM bind_fn $
 185     do { reft <- unifyList emptyInternalReft cos tys1 tys2
 186
 187         -- Find the fixed point of the resulting non-idempotent substitution
 188         ; let in_scope = mkInScopeSet (tvs1 `unionVarSet` tvs2)
 189               tv_env   = fixTvSubstEnv in_scope (mapVarEnv snd reft)
 190
 191         ; return (mkTvSubst in_scope tv_env) }
 192   where
 193     tvs1 = tyVarsOfTypes tys1
 194     tvs2 = tyVarsOfTypes tys2
 195     cos  = zipWith mkUnsafeCoercion tys1 tys2
 196
 197
 198 ----------------------------
 199 fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv
 200         -- Find the fixed point of a TvSubstEnv
 201         -- (assuming it has no loops!)
 202 fixTvSubstEnv in_scope env
 203   = fixpt
 204   where
 205     fixpt = mapVarEnv (substTy (mkTvSubst in_scope fixpt)) env
 206
 207 ----------------------------
 208 dataConCanMatch :: DataCon -> [Type] -> Bool
 209 -- Returns True iff the data con can match a scrutinee of type (T tys)
 210 --                  where T is the type constructor for the data con
 211 --
 212 -- Instantiate the equations and try to unify them
 213 dataConCanMatch con tys
 214   = isJust (tcUnifyTys (\tv -> BindMe)
 215                        (map (substTyVar subst . fst) eq_spec)
 216                        (map snd eq_spec))
 217   where
 218     dc_tvs  = dataConUnivTyVars con
 219     eq_spec = dataConEqSpec con
 220     subst   = zipTopTvSubst dc_tvs tys
 221
 222 ----------------------------
 223 tryToBind :: TyVarSet -> TyVar -> BindFlag
 224 tryToBind tv_set tv | tv `elemVarSet` tv_set = BindMe
 225                     | otherwise              = AvoidMe
 226 \end{code}
 227
 228
 229 %************************************************************************
 230 %*                                                                      *
 231                 The workhorse
 232 %*                                                                      *
 233 %************************************************************************
 234
 235 \begin{code}
 236 type InternalReft = TyVarEnv (Coercion, Type)
 237
 238 -- INVARIANT:   a->(co,ty)   then   co :: (a:=:ty)
 239 -- Not necessarily idemopotent
 240
 241 emptyInternalReft :: InternalReft
 242 emptyInternalReft = emptyVarEnv
 243
 244 unify :: InternalReft           -- An existing substitution to extend
 245       -> Coercion       -- Witness of their equality
 246       -> Type -> Type   -- Types to be unified, and witness of their equality
 247       -> UM InternalReft                -- Just the extended substitution,
 248                                 -- Nothing if unification failed
 249 -- We do not require the incoming substitution to be idempotent,
 250 -- nor guarantee that the outgoing one is.  That's fixed up by
 251 -- the wrappers.
 252
 253 -- PRE-CONDITION: in the call (unify r co ty1 ty2), we know that
 254 --                      co :: (ty1:=:ty2)
 255
 256 -- Respects newtypes, PredTypes
 257
 258 unify subst co ty1 ty2 = -- pprTrace "unify" (ppr subst <+> pprParendType ty1 <+> pprParendType ty2) $
 259                          unify_ subst co ty1 ty2
 260
 261 -- in unify_, any NewTcApps/Preds should be taken at face value
 262 unify_ subst co (TyVarTy tv1) ty2  = uVar False subst co tv1 ty2
 263 unify_ subst co ty1 (TyVarTy tv2)  = uVar True  subst co tv2 ty1
 264
 265 unify_ subst co ty1 ty2 | Just ty1' <- tcView ty1 = unify subst co ty1' ty2
 266 unify_ subst co ty1 ty2 | Just ty2' <- tcView ty2 = unify subst co ty1 ty2'
 267
 268 unify_ subst co (PredTy p1) (PredTy p2) = unify_pred subst co p1 p2
 269
 270 unify_ subst co t1@(TyConApp tyc1 tys1) t2@(TyConApp tyc2 tys2)
 271   | tyc1 == tyc2 = unify_tys subst co tys1 tys2
 272
 273 unify_ subst co (FunTy ty1a ty1b) (FunTy ty2a ty2b)
 274   = do  { let [co1,co2] = decomposeCo 2 co
 275         ; subst' <- unify subst co1 ty1a ty2a
 276         ; unify subst' co2 ty1b ty2b }
 277
 278         -- Applications need a bit of care!
 279         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
 280         -- NB: we've already dealt with type variables and Notes,
 281         -- so if one type is an App the other one jolly well better be too
 282 unify_ subst co (AppTy ty1a ty1b) ty2
 283   | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
 284   = do  { subst' <- unify subst (mkLeftCoercion co) ty1a ty2a
 285         ; unify subst' (mkRightCoercion co) ty1b ty2b }
 286
 287 unify_ subst co ty1 (AppTy ty2a ty2b)
 288   | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
 289   = do  { subst' <- unify subst (mkLeftCoercion co) ty1a ty2a
 290         ; unify subst' (mkRightCoercion co) ty1b ty2b }
 291
 292 unify_ subst co ty1 ty2 = failWith (misMatch ty1 ty2)
 293         -- ForAlls??
 294
 295
 296 ------------------------------
 297 unify_pred subst co (ClassP c1 tys1) (ClassP c2 tys2)
 298   | c1 == c2 = unify_tys subst co tys1 tys2
 299 unify_pred subst co (IParam n1 t1) (IParam n2 t2)
 300   | n1 == n2 = unify subst co t1 t2
 301 unify_pred subst co p1 p2 = failWith (misMatch (PredTy p1) (PredTy p2))
 302
 303 ------------------------------
 304 unify_tys :: InternalReft -> Coercion -> [Type] -> [Type] -> UM InternalReft
 305 unify_tys subst co xs ys
 306   = unifyList subst (decomposeCo (length xs) co) xs ys
 307
 308 unifyList :: InternalReft -> [Coercion] -> [Type] -> [Type] -> UM InternalReft
 309 unifyList subst orig_cos orig_xs orig_ys
 310   = go subst orig_cos orig_xs orig_ys
 311   where
 312     go subst _        []     []     = return subst
 313     go subst (co:cos) (x:xs) (y:ys) = do { subst' <- unify subst co x y
 314                                          ; go subst' cos xs ys }
 315     go subst _ _ _ = failWith (lengthMisMatch orig_xs orig_ys)
 316
 317 ---------------------------------
 318 uVar :: Bool            -- Swapped
 319      -> InternalReft    -- An existing substitution to extend
 320      -> Coercion
 321      -> TyVar           -- Type variable to be unified
 322      -> Type            -- with this type
 323      -> UM InternalReft
 324
 325 -- PRE-CONDITION: in the call (uVar swap r co tv1 ty), we know that
 326 --      if swap=False   co :: (tv1:=:ty)
 327 --      if swap=True    co :: (ty:=:tv1)
 328
 329 uVar swap subst co tv1 ty
 330  = -- Check to see whether tv1 is refined by the substitution
 331    case (lookupVarEnv subst tv1) of
 332
 333      -- Yes, call back into unify'
 334      Just (co',ty')     -- co' :: (tv1:=:ty')
 335         | swap          -- co :: (ty:=:tv1)
 336         -> unify subst (mkTransCoercion co co') ty ty'
 337         | otherwise     -- co :: (tv1:=:ty)
 338         -> unify subst (mkTransCoercion (mkSymCoercion co') co) ty' ty
 339
 340      -- No, continue
 341      Nothing -> uUnrefined subst (if swap then mkSymCoercion co else co)
 342                            tv1 ty ty
 343
 344
 345 uUnrefined :: InternalReft        -- An existing substitution to extend
 346            -> Coercion
 347            -> TyVar               -- Type variable to be unified
 348            -> Type                -- with this type
 349            -> Type                -- (de-noted version)
 350            -> UM InternalReft
 351
 352 -- We know that tv1 isn't refined
 353 -- PRE-CONDITION: in the call (uUnrefined r co tv ty ty'), we know that
 354 --      co :: tv:=:ty
 355
 356 uUnrefined subst co tv1 ty2 ty2'
 357   | Just ty2'' <- tcView ty2'
 358   = uUnrefined subst co tv1 ty2 ty2''   -- Unwrap synonyms
 359                 -- This is essential, in case we have
 360                 --      type Foo a = a
 361                 -- and then unify a :=: Foo a
 362
 363 uUnrefined subst co tv1 ty2 (TyVarTy tv2)
 364   | tv1 == tv2          -- Same type variable
 365   = return subst
 366
 367     -- Check to see whether tv2 is refined
 368   | Just (co',ty') <- lookupVarEnv subst tv2
 369   = uUnrefined subst (mkTransCoercion co co') tv1 ty' ty'
 370
 371   -- So both are unrefined; next, see if the kinds force the direction
 372   | eqKind k1 k2        -- Can update either; so check the bind-flags
 373   = do  { b1 <- tvBindFlag tv1
 374         ; b2 <- tvBindFlag tv2
 375         ; case (b1,b2) of
 376             (BindMe, _)          -> bind tv1 ty2
 377
 378             (AvoidMe, BindMe)    -> bind tv2 ty1
 379             (AvoidMe, _)         -> bind tv1 ty2
 380
 381             (WildCard, WildCard) -> return subst
 382             (WildCard, Skolem)   -> return subst
 383             (WildCard, _)        -> bind tv2 ty1
 384
 385             (Skolem, WildCard)   -> return subst
 386             (Skolem, Skolem)     -> failWith (misMatch ty1 ty2)
 387             (Skolem, _)          -> bind tv2 ty1
 388         }
 389
 390   | k1 `isSubKind` k2 = bindTv subst co tv2 ty1 -- Must update tv2
 391   | k2 `isSubKind` k1 = bindTv subst co tv1 ty2 -- Must update tv1
 392
 393   | otherwise = failWith (kindMisMatch tv1 ty2)
 394   where
 395     ty1 = TyVarTy tv1
 396     k1 = tyVarKind tv1
 397     k2 = tyVarKind tv2
 398     bind tv ty = return (extendVarEnv subst tv (co,ty))
 399
 400 uUnrefined subst co tv1 ty2 ty2'        -- ty2 is not a type variable
 401   | tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2')
 402   = failWith (occursCheck tv1 ty2)      -- Occurs check
 403   | not (k2 `isSubKind` k1)
 404   = failWith (kindMisMatch tv1 ty2)     -- Kind check
 405   | otherwise
 406   = bindTv subst co tv1 ty2             -- Bind tyvar to the synonym if poss
 407   where
 408     k1 = tyVarKind tv1
 409     k2 = typeKind ty2'
 410
 411 substTvSet :: InternalReft -> TyVarSet -> TyVarSet
 412 -- Apply the non-idempotent substitution to a set of type variables,
 413 -- remembering that the substitution isn't necessarily idempotent
 414 substTvSet subst tvs
 415   = foldVarSet (unionVarSet . get) emptyVarSet tvs
 416   where
 417     get tv = case lookupVarEnv subst tv of
 418                 Nothing     -> unitVarSet tv
 419                 Just (_,ty) -> substTvSet subst (tyVarsOfType ty)
 420
 421 bindTv subst co tv ty   -- ty is not a type variable
 422   = do  { b <- tvBindFlag tv
 423         ; case b of
 424             Skolem   -> failWith (misMatch (TyVarTy tv) ty)
 425             WildCard -> return subst
 426             other    -> return (extendVarEnv subst tv (co,ty))
 427         }
 428 \end{code}
 429
 430 %************************************************************************
 431 %*                                                                      *
 432                 Unification monad
 433 %*                                                                      *
 434 %************************************************************************
 435
 436 \begin{code}
 437 data BindFlag
 438   = BindMe      -- A regular type variable
 439   | AvoidMe     -- Like BindMe but, given the choice, avoid binding it
 440
 441   | Skolem      -- This type variable is a skolem constant
 442                 -- Don't bind it; it only matches itself
 443
 444   | WildCard    -- This type variable matches anything,
 445                 -- and does not affect the substitution
 446
 447 newtype UM a = UM { unUM :: (TyVar -> BindFlag)
 448                          -> MaybeErr Message a }
 449
 450 instance Monad UM where
 451   return a = UM (\tvs -> Succeeded a)
 452   fail s   = UM (\tvs -> Failed (text s))
 453   m >>= k  = UM (\tvs -> case unUM m tvs of
 454                            Failed err -> Failed err
 455                            Succeeded v  -> unUM (k v) tvs)
 456
 457 initUM :: (TyVar -> BindFlag) -> UM a -> MaybeErr Message a
 458 initUM badtvs um = unUM um badtvs
 459
 460 tvBindFlag :: TyVar -> UM BindFlag
 461 tvBindFlag tv = UM (\tv_fn -> Succeeded (tv_fn tv))
 462
 463 failWith :: Message -> UM a
 464 failWith msg = UM (\tv_fn -> Failed msg)
 465
 466 maybeErrToMaybe :: MaybeErr fail succ -> Maybe succ
 467 maybeErrToMaybe (Succeeded a) = Just a
 468 maybeErrToMaybe (Failed m)    = Nothing
 469 \end{code}
 470
 471
 472 %************************************************************************
 473 %*                                                                      *
 474                 Error reporting
 475         We go to a lot more trouble to tidy the types
 476         in TcUnify.  Maybe we'll end up having to do that
 477         here too, but I'll leave it for now.
 478 %*                                                                      *
 479 %************************************************************************
 480
 481 \begin{code}
 482 misMatch t1 t2
 483   = ptext SLIT("Can't match types") <+> quotes (ppr t1) <+>
 484     ptext SLIT("and") <+> quotes (ppr t2)
 485
 486 lengthMisMatch tys1 tys2
 487   = sep [ptext SLIT("Can't match unequal length lists"),
 488          nest 2 (ppr tys1), nest 2 (ppr tys2) ]
 489
 490 kindMisMatch tv1 t2
 491   = vcat [ptext SLIT("Can't match kinds") <+> quotes (ppr (tyVarKind tv1)) <+>
 492             ptext SLIT("and") <+> quotes (ppr (typeKind t2)),
 493           ptext SLIT("when matching") <+> quotes (ppr tv1) <+>
 494                 ptext SLIT("with") <+> quotes (ppr t2)]
 495
 496 occursCheck tv ty
 497   = hang (ptext SLIT("Can't construct the infinite type"))
 498        2 (ppr tv <+> equals <+> ppr ty)
 499 \end{code}