Comments only
[ghc-hetmet.git] / compiler / specialise / SpecConstr.lhs
index 219e758..cbe1c0b 100644 (file)
@@ -1,3 +1,8 @@
+ToDo [Nov 2010]
+~~~~~~~~~~~~~~~
+1. Use a library type rather than an annotation for ForceSpecConstr
+2. Nuke NoSpecConstr
+
 %
 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
 %
 -- for details
 
 module SpecConstr(
-       specConstrProgram, SpecConstrAnnotation(..)
+       specConstrProgram
+#ifdef GHCI
+        , SpecConstrAnnotation(..)
+#endif
     ) where
 
 #include "HsVersions.h"
@@ -24,18 +32,17 @@ import CoreFVs              ( exprsFreeVars )
 import CoreMonad
 import HscTypes         ( ModGuts(..) )
 import WwLib           ( mkWorkerArgs )
-import DataCon         ( dataConTyCon, dataConRepArity, dataConUnivTyVars )
-import TyCon            ( TyCon )
-import Literal          ( literalType )
+import DataCon
 import Coercion        
 import Rules
 import Type            hiding( substTy )
 import Id
-import MkId            ( mkImpossibleExpr )
+import MkCore          ( mkImpossibleExpr )
 import Var
 import VarEnv
 import VarSet
 import Name
+import BasicTypes
 import DynFlags                ( DynFlags(..) )
 import StaticFlags     ( opt_PprStyle_Debug )
 import Maybes          ( orElse, catMaybes, isJust, isNothing )
@@ -47,14 +54,18 @@ import UniqSupply
 import Outputable
 import FastString
 import UniqFM
-import qualified LazyUniqFM as L
 import MonadUtils
 import Control.Monad   ( zipWithM )
 import Data.List
-#if __GLASGOW_HASKELL__ > 609
-import Data.Data        ( Data, Typeable )
+
+
+-- See Note [SpecConstrAnnotation]
+#ifndef GHCI
+type SpecConstrAnnotation = ()
 #else
-import Data.Generics    ( Data, Typeable )
+import Literal          ( literalType )
+import TyCon            ( TyCon )
+import GHC.Exts( SpecConstrAnnotation(..) )
 #endif
 \end{code}
 
@@ -389,6 +400,17 @@ But fspec doesn't have decent strictnes info.  As it happened,
 and hence f.  But now f's strictness is less than its arity, which
 breaks an invariant.
 
+Note [SpecConstrAnnotation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+SpecConstrAnnotation is defined in GHC.Exts, and is only guaranteed to
+be available in stage 2 (well, until the bootstrap compiler can be
+guaranteed to have it)
+
+So we define it to be () in stage1 (ie when GHCI is undefined), and
+'#ifdef' out the code that uses it.
+
+See also Note [Forcing specialisation]
+
 Note [Forcing specialisation]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 With stream fusion and in other similar cases, we want to fully specialise
@@ -404,22 +426,83 @@ loop. Here is a (simplified) example from the vector library:
   {-# INLINE foldl #-}
   foldl f z (Stream step s _) = foldl_loop SPEC z s
     where
-      foldl_loop SPEC z s = case step s of
-                              Yield x s' -> foldl_loop SPEC (f z x) s'
-                              Skip       -> foldl_loop SPEC z s'
+      foldl_loop !sPEC z s = case step s of
+                              Yield x s' -> foldl_loop sPEC (f z x) s'
+                              Skip       -> foldl_loop sPEC z s'
                               Done       -> z
 
 SpecConstr will spot the SPEC parameter and always fully specialise
-foldl_loop. Note that we can't just annotate foldl_loop since it isn't a
-top-level function but even if we could, inlining etc. could easily drop the
-annotation. We also have to prevent the SPEC argument from being removed by
-w/w which is why SPEC is a sum type. This is all quite ugly; we ought to come
-up with a better design.
+foldl_loop. Note that
+
+  * We have to prevent the SPEC argument from being removed by
+    w/w which is why (a) SPEC is a sum type, and (b) we have to seq on
+    the SPEC argument.
+
+  * And lastly, the SPEC argument is ultimately eliminated by
+    SpecConstr itself so there is no runtime overhead.
+
+This is all quite ugly; we ought to come up with a better design.
 
 ForceSpecConstr arguments are spotted in scExpr' and scTopBinds which then set
-force_spec to True when calling specLoop. This flag makes specLoop and
-specialise ignore specConstrCount and specConstrThreshold when deciding
-whether to specialise a function.
+sc_force to True when calling specLoop. This flag does three things:
+  * Ignore specConstrThreshold, to specialise functions of arbitrary size
+        (see scTopBind)
+  * Ignore specConstrCount, to make arbitrary numbers of specialisations
+        (see specialise)
+  * Specialise even for arguments that are not scrutinised in the loop
+        (see argToPat; Trac #4488)
+
+What alternatives did I consider? Annotating the loop itself doesn't
+work because (a) it is local and (b) it will be w/w'ed and I having
+w/w propagating annotation somehow doesn't seem like a good idea. The
+types of the loop arguments really seem to be the most persistent
+thing.
+
+Annotating the types that make up the loop state doesn't work,
+either, because (a) it would prevent us from using types like Either
+or tuples here, (b) we don't want to restrict the set of types that
+can be used in Stream states and (c) some types are fixed by the user
+(e.g., the accumulator here) but we still want to specialise as much
+as possible.
+
+ForceSpecConstr is done by way of an annotation:
+  data SPEC = SPEC | SPEC2
+  {-# ANN type SPEC ForceSpecConstr #-}
+But SPEC is the *only* type so annotated, so it'd be better to
+use a particular library type.
+
+Alternatives to ForceSpecConstr
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Instead of giving the loop an extra argument of type SPEC, we
+also considered *wrapping* arguments in SPEC, thus
+  data SPEC a = SPEC a | SPEC2
+
+  loop = \arg -> case arg of
+                     SPEC state ->
+                        case state of (x,y) -> ... loop (SPEC (x',y')) ...
+                        S2 -> error ...
+The idea is that a SPEC argument says "specialise this argument
+regardless of whether the function case-analyses it.  But this
+doesn't work well:
+  * SPEC must still be a sum type, else the strictness analyser
+    eliminates it
+  * But that means that 'loop' won't be strict in its real payload
+This loss of strictness in turn screws up specialisation, because
+we may end up with calls like
+   loop (SPEC (case z of (p,q) -> (q,p)))
+Without the SPEC, if 'loop' was strict, the case would move out
+and we'd see loop applied to a pair. But if 'loop' isn' strict
+this doesn't look like a specialisable call.
+
+Note [NoSpecConstr]
+~~~~~~~~~~~~~~~~~~~
+The ignoreAltCon stuff allows you to say
+    {-# ANN type T NoSpecConstr #-}
+to mean "don't specialise on arguments of this type.  It was added
+before we had ForceSpecConstr.  Lacking ForceSpecConstr we specialised
+regardless of size; and then we needed a way to turn that *off*.  Now
+that we have ForceSpecConstr, this NoSpecConstr is probably redundant.
+(Used only for PArray.)
 
 -----------------------------------------------------
                Stuff not yet handled
@@ -498,20 +581,6 @@ unbox the strict fields, becuase T is polymorphic!)
 
 %************************************************************************
 %*                                                                     *
-\subsection{Annotations}
-%*                                                                     *
-%************************************************************************
-
-Annotating a type with NoSpecConstr will make SpecConstr not specialise
-for arguments of that type.
-
-\begin{code}
-data SpecConstrAnnotation = NoSpecConstr | ForceSpecConstr
-                deriving( Data, Typeable, Eq )
-\end{code}
-
-%************************************************************************
-%*                                                                     *
 \subsection{Top level wrapper stuff}
 %*                                                                     *
 %************************************************************************
@@ -543,6 +612,8 @@ specConstrProgram guts
 data ScEnv = SCE { sc_size  :: Maybe Int,      -- Size threshold
                   sc_count :: Maybe Int,       -- Max # of specialisations for any one fn
                                                -- See Note [Avoiding exponential blowup]
+                   sc_force :: Bool,            -- Force specialisation?
+                                                -- See Note [Forcing specialisation]
 
                   sc_subst :: Subst,           -- Current substitution
                                                -- Maps InIds to OutExprs
@@ -555,7 +626,7 @@ data ScEnv = SCE { sc_size  :: Maybe Int,   -- Size threshold
                        -- Domain is OutIds (*after* applying the substitution)
                        -- Used even for top-level bindings (but not imported ones)
 
-                   sc_annotations :: L.UniqFM SpecConstrAnnotation
+                   sc_annotations :: UniqFM SpecConstrAnnotation
             }
 
 ---------------------
@@ -573,6 +644,7 @@ type HowBoundEnv = VarEnv HowBound  -- Domain is OutVars
 ---------------------
 type ValueEnv = IdEnv Value            -- Domain is OutIds
 data Value    = ConVal AltCon [CoreArg]        -- _Saturated_ constructors
+                                       --   The AltCon is never DEFAULT
              | LambdaVal               -- Inlinable lambdas or PAPs
 
 instance Outputable Value where
@@ -580,10 +652,11 @@ instance Outputable Value where
    ppr LambdaVal        = ptext (sLit "<Lambda>")
 
 ---------------------
-initScEnv :: DynFlags -> L.UniqFM SpecConstrAnnotation -> ScEnv
+initScEnv :: DynFlags -> UniqFM SpecConstrAnnotation -> ScEnv
 initScEnv dflags anns
   = SCE { sc_size = specConstrThreshold dflags,
          sc_count = specConstrCount dflags,
+          sc_force = False,
          sc_subst = emptySubst, 
          sc_how_bound = emptyVarEnv, 
          sc_vals = emptyVarEnv,
@@ -599,6 +672,9 @@ instance Outputable HowBound where
   ppr RecFun = text "RecFun"
   ppr RecArg = text "RecArg"
 
+scForce :: ScEnv -> Bool -> ScEnv
+scForce env b = env { sc_force = b }
+
 lookupHowBound :: ScEnv -> Id -> Maybe HowBound
 lookupHowBound env id = lookupVarEnv (sc_how_bound env) id
 
@@ -676,7 +752,7 @@ extendCaseBndrs env case_bndr con alt_bndrs
        --      Var v  -> extendValEnv env1 v cval
        --      _other -> env1
  where
-   zap v | isTyVar v = v               -- See NB2 above
+   zap v | isTyCoVar v = v             -- See NB2 above
          | otherwise = zapIdOccInfo v
    env1 = extendValEnv env case_bndr cval
    cval = case con of
@@ -687,22 +763,41 @@ extendCaseBndrs env case_bndr con alt_bndrs
                        vanilla_args = map Type (tyConAppArgs (idType case_bndr)) ++
                                       varsToCoreExprs alt_bndrs
 
-ignoreTyCon :: ScEnv -> TyCon -> Bool
-ignoreTyCon env tycon
-  = L.lookupUFM (sc_annotations env) tycon == Just NoSpecConstr
 
-ignoreType :: ScEnv -> Type -> Bool
+decreaseSpecCount :: ScEnv -> Int -> ScEnv
+-- See Note [Avoiding exponential blowup]
+decreaseSpecCount env n_specs 
+  = env { sc_count = case sc_count env of
+                       Nothing -> Nothing
+                       Just n  -> Just (n `div` (n_specs + 1)) }
+       -- The "+1" takes account of the original function; 
+       -- See Note [Avoiding exponential blowup]
+
+---------------------------------------------------
+-- See Note [SpecConstrAnnotation]
+ignoreType    :: ScEnv -> Type   -> Bool
+ignoreAltCon  :: ScEnv -> AltCon -> Bool
+forceSpecBndr :: ScEnv -> Var    -> Bool
+#ifndef GHCI
+ignoreType    _ _ = False
+ignoreAltCon  _ _ = False
+forceSpecBndr _ _ = False
+
+#else /* GHCI */
+
+ignoreAltCon env (DataAlt dc) = ignoreTyCon env (dataConTyCon dc)
+ignoreAltCon env (LitAlt lit) = ignoreType env (literalType lit)
+ignoreAltCon _   DEFAULT      = panic "ignoreAltCon"  -- DEFAULT cannot be in a ConVal
+
 ignoreType env ty
   = case splitTyConApp_maybe ty of
       Just (tycon, _) -> ignoreTyCon env tycon
       _               -> False
 
-ignoreAltCon :: ScEnv -> AltCon -> Bool
-ignoreAltCon env (DataAlt dc) = ignoreTyCon env (dataConTyCon dc)
-ignoreAltCon env (LitAlt lit) = ignoreType env (literalType lit)
-ignoreAltCon _   DEFAULT      = True
+ignoreTyCon :: ScEnv -> TyCon -> Bool
+ignoreTyCon env tycon
+  = lookupUFM (sc_annotations env) tycon == Just NoSpecConstr
 
-forceSpecBndr :: ScEnv -> Var -> Bool
 forceSpecBndr env var = forceSpecFunTy env . snd . splitForAllTys . varType $ var
 
 forceSpecFunTy :: ScEnv -> Type -> Bool
@@ -715,19 +810,11 @@ forceSpecArgTy env ty
 forceSpecArgTy env ty
   | Just (tycon, tys) <- splitTyConApp_maybe ty
   , tycon /= funTyCon
-      = L.lookupUFM (sc_annotations env) tycon == Just ForceSpecConstr
+      = lookupUFM (sc_annotations env) tycon == Just ForceSpecConstr
         || any (forceSpecArgTy env) tys
 
 forceSpecArgTy _ _ = False
-
-decreaseSpecCount :: ScEnv -> Int -> ScEnv
--- See Note [Avoiding exponential blowup]
-decreaseSpecCount env n_specs 
-  = env { sc_count = case sc_count env of
-                       Nothing -> Nothing
-                       Just n  -> Just (n `div` (n_specs + 1)) }
-       -- The "+1" takes account of the original function; 
-       -- See Note [Avoiding exponential blowup]
+#endif /* GHCI */
 \end{code}
 
 Note [Avoiding exponential blowup]
@@ -940,21 +1027,25 @@ scExpr' env (Case scrut b ty alts)
           ; return (usg', scrut_occ, (con, bs2, rhs')) }
 
 scExpr' env (Let (NonRec bndr rhs) body)
-  | isTyVar bndr       -- Type-lets may be created by doBeta
+  | isTyCoVar bndr     -- Type-lets may be created by doBeta
   = scExpr' (extendScSubst env bndr rhs) body
 
-  | otherwise             -- Note [Local let bindings]
+  | otherwise  
   = do { let (body_env, bndr') = extendBndr env bndr
-             body_env2 = extendHowBound body_env [bndr'] RecFun
-       ; (body_usg, body') <- scExpr body_env2 body
-
        ; (rhs_usg, rhs_info) <- scRecRhs env (bndr',rhs)
 
+       ; let body_env2 = extendHowBound body_env [bndr'] RecFun
+                                  -- Note [Local let bindings]
+             RI _ rhs' _ _ _ = rhs_info
+              body_env3 = extendValEnv body_env2 bndr' (isValue (sc_vals env) rhs')
+
+       ; (body_usg, body') <- scExpr body_env3 body
+
           -- NB: We don't use the ForceSpecConstr mechanism (see
           -- Note [Forcing specialisation]) for non-recursive bindings
           -- at the moment. I'm not sure if this is the right thing to do.
-       ; let force_spec = False
-       ; (spec_usg, specs) <- specialise env force_spec 
+       ; let env' = scForce env False
+       ; (spec_usg, specs) <- specialise env'
                                           (scu_calls body_usg) 
                                          rhs_info
                                           (SI [] 0 (Just rhs_usg))
@@ -977,7 +1068,7 @@ scExpr' env (Let (Rec prs) body)
        ; (body_usg, body')     <- scExpr rhs_env2 body
 
        -- NB: start specLoop from body_usg
-       ; (spec_usg, specs) <- specLoop rhs_env2 force_spec
+       ; (spec_usg, specs) <- specLoop (scForce rhs_env2 force_spec)
                                         (scu_calls body_usg) rhs_infos nullUsage
                                        [SI [] 0 (Just usg) | usg <- rhs_usgs]
                -- Do not unconditionally use rhs_usgs. 
@@ -1066,7 +1157,7 @@ scTopBind env (Rec prs)
        ; (rhs_usgs, rhs_infos) <- mapAndUnzipM (scRecRhs rhs_env2) (bndrs' `zip` rhss)
        ; let rhs_usg = combineUsages rhs_usgs
 
-       ; (_, specs) <- specLoop rhs_env2 force_spec
+       ; (_, specs) <- specLoop (scForce rhs_env2 force_spec)
                                  (scu_calls rhs_usg) rhs_infos nullUsage
                                 [SI [] 0 Nothing | _ <- bndrs]
 
@@ -1144,14 +1235,12 @@ data OneSpec  = OS CallPat              -- Call pattern that generated this specialisation
 
 
 specLoop :: ScEnv
-         -> Bool                                -- force specialisation?
-                                                -- Note [Forcing specialisation]
         -> CallEnv
         -> [RhsInfo]
         -> ScUsage -> [SpecInfo]               -- One per binder; acccumulating parameter
         -> UniqSM (ScUsage, [SpecInfo])        -- ...ditto...
-specLoop env force_spec all_calls rhs_infos usg_so_far specs_so_far
-  = do { specs_w_usg <- zipWithM (specialise env force_spec all_calls) rhs_infos specs_so_far
+specLoop env all_calls rhs_infos usg_so_far specs_so_far
+  = do { specs_w_usg <- zipWithM (specialise env all_calls) rhs_infos specs_so_far
        ; let (new_usg_s, all_specs) = unzip specs_w_usg
              new_usg   = combineUsages new_usg_s
              new_calls = scu_calls new_usg
@@ -1159,12 +1248,10 @@ specLoop env force_spec all_calls rhs_infos usg_so_far specs_so_far
        ; if isEmptyVarEnv new_calls then
                return (all_usg, all_specs) 
          else 
-               specLoop env force_spec new_calls rhs_infos all_usg all_specs }
+               specLoop env new_calls rhs_infos all_usg all_specs }
 
 specialise 
    :: ScEnv
-   -> Bool                              -- force specialisation?
-                                        --   Note [Forcing specialisation]
    -> CallEnv                          -- Info on calls
    -> RhsInfo
    -> SpecInfo                         -- Original RHS plus patterns dealt with
@@ -1174,9 +1261,10 @@ specialise
 -- So when we make a specialised copy of the RHS, we're starting
 -- from an RHS whose nested functions have been optimised already.
 
-specialise env force_spec bind_calls (RI fn _ arg_bndrs body arg_occs) 
-                         spec_info@(SI specs spec_count mb_unspec)
+specialise env bind_calls (RI fn _ arg_bndrs body arg_occs) 
+               spec_info@(SI specs spec_count mb_unspec)
   | not (isBottomingId fn)      -- Note [Do not specialise diverging functions]
+  , not (isNeverActive (idInlineActivation fn))        -- See Note [Transfer activation]
   , notNull arg_bndrs          -- Only specialise functions
   , Just all_calls <- lookupVarEnv bind_calls fn
   = do { (boring_call, pats) <- callsToPats env specs arg_occs all_calls
@@ -1190,7 +1278,7 @@ specialise env force_spec bind_calls (RI fn _ arg_bndrs body arg_occs)
        ; let n_pats      = length pats
               spec_count' = n_pats + spec_count
        ; case sc_count env of
-           Just max | not force_spec && spec_count' > max
+           Just max | not (sc_force env) && spec_count' > max
                -> pprTrace "SpecConstr" msg $  
                    return (nullUsage, spec_info)
                where
@@ -1282,7 +1370,9 @@ spec_one env fn arg_bndrs body (call_pat@(qvars, pats), rule_number)
              body_ty    = exprType spec_body
              rule_rhs   = mkVarApps (Var spec_id) spec_call_args
               inline_act = idInlineActivation fn
-             rule       = mkLocalRule rule_name inline_act fn_name qvars pats rule_rhs
+             rule       = mkRule True {- Auto -} True {- Local -}
+                                  rule_name inline_act fn_name qvars pats rule_rhs
+                          -- See Note [Transfer activation]
        ; return (spec_usg, OS call_pat rule spec_id spec_rhs) }
 
 calcSpecStrictness :: Id                    -- The original function
@@ -1318,6 +1408,10 @@ specialised RHS, and that can lead directly to exponential behaviour.
 
 Note [Transfer activation]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
+  This note is for SpecConstr, but exactly the same thing
+  happens in the overloading specialiser; see
+  Note [Auto-specialisation and RULES] in Specialise.
+
 In which phase should the specialise-constructor rules be active?
 Originally I made them always-active, but Manuel found that this
 defeated some clever user-written rules.  Then I made them active only
@@ -1328,8 +1422,9 @@ simplCore/should_compile/spec-inline.
 
 So now I just use the inline-activation of the parent Id, as the
 activation for the specialiation RULE, just like the main specialiser;
-see Note [Auto-specialisation and RULES] in Specialise.
 
+This in turn means there is no point in specialising NOINLINE things,
+so we test for that.
 
 Note [Transfer strictness]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1395,7 +1490,7 @@ callToPats env bndr_occs (con_env, args)
                -- at the call site
                -- See Note [Shadowing] at the top
                
-             (tvs, ids) = partition isTyVar qvars
+             (tvs, ids) = partition isTyCoVar qvars
              qvars'     = tvs ++ ids
                -- Put the type variables first; the type of a term
                -- variable may mention a type variable
@@ -1441,11 +1536,18 @@ argToPat env in_scope val_env (Note _ arg) arg_occ
 
 argToPat env in_scope val_env (Let _ arg) arg_occ
   = argToPat env in_scope val_env arg arg_occ
+       -- See Note [Matching lets] in Rule.lhs
        -- Look through let expressions
-       -- e.g.         f (let v = rhs in \y -> ...v...)
-       -- Here we can specialise for f (\y -> ...)
+       -- e.g.         f (let v = rhs in (v,w))
+       -- Here we can specialise for f (v,w)
        -- because the rule-matcher will look through the let.
 
+{- Disabled; see Note [Matching cases] in Rule.lhs
+argToPat env in_scope val_env (Case scrut _ _ [(_, _, rhs)]) arg_occ
+  | exprOkForSpeculation scrut -- See Note [Matching cases] in Rule.hhs
+  = argToPat env in_scope val_env rhs arg_occ
+-}
+
 argToPat env in_scope val_env (Cast arg co) arg_occ
   | not (ignoreType env ty2)
   = do { (interesting, arg') <- argToPat env in_scope val_env arg arg_occ
@@ -1478,15 +1580,19 @@ argToPat in_scope val_env arg arg_occ
   -- NB: this *precedes* the Var case, so that we catch nullary constrs
 argToPat env in_scope val_env arg arg_occ
   | Just (ConVal dc args) <- isValue val_env arg
-  , not (ignoreAltCon env dc)
-  , case arg_occ of
-       ScrutOcc _ -> True              -- Used only by case scrutinee
-       BothOcc    -> case arg of       -- Used elsewhere
-                       App {} -> True  --     see Note [Reboxing]
-                       _other -> False
-       _other     -> False     -- No point; the arg is not decomposed
+  , not (ignoreAltCon env dc)        -- See Note [NoSpecConstr]
+  , sc_force env || scrutinised
   = do { args' <- argsToPats env in_scope val_env (args `zip` conArgOccs arg_occ dc)
        ; return (True, mk_con_app dc (map snd args')) }
+  where
+    scrutinised
+      = case arg_occ of
+          ScrutOcc _ -> True           -- Used only by case scrutinee
+          BothOcc    -> case arg of    -- Used elsewhere
+                          App {} -> True       --     see Note [Reboxing]
+                          _other -> False
+          _other     -> False           -- No point; the arg is not decomposed
+
 
   -- Check if the argument is a variable that 
   -- is in scope at the function definition site
@@ -1494,8 +1600,8 @@ argToPat env in_scope val_env arg arg_occ
   --   (a) it's used in an interesting way in the body
   --   (b) we know what its value is
 argToPat env in_scope val_env (Var v) arg_occ
-  | case arg_occ of { UnkOcc -> False; _other -> True },       -- (a)
-    is_value,                                                  -- (b)
+  | sc_force env || case arg_occ of { UnkOcc -> False; _other -> True }, -- (a)
+    is_value,                                                            -- (b)
     not (ignoreType env (varType v))
   = return (True, Var v)
   where
@@ -1562,7 +1668,7 @@ isValue env (Var v)
        -- as well, for let-bound constructors!
 
 isValue env (Lam b e)
-  | isTyVar b = case isValue env e of
+  | isTyCoVar b = case isValue env e of
                  Just _  -> Just LambdaVal
                  Nothing -> Nothing
   | otherwise = Just LambdaVal