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