diff --git a/src/compiler/api/GF/Compile/Compute/Concrete2.hs b/src/compiler/api/GF/Compile/Compute/Concrete2.hs
index ee7e4b024..394c4088d 100644
--- a/src/compiler/api/GF/Compile/Compute/Concrete2.hs
+++ b/src/compiler/api/GF/Compile/Compute/Concrete2.hs
@@ -3,20 +3,22 @@
 module GF.Compile.Compute.Concrete2
            (Env, Scope, Value(..), Variants(..), Constraint, OptionInfo(..), ChoiceMap, cleanOptions,
             ConstValue(..), ConstVariants(..), Globals(..), PredefTable, EvalM,
-            mapVariants, unvariants, variants2consts, consts2variants,
-            runEvalM, runEvalMWithOpts, stdPredef, globals, withState,
+            mapVariants, mapVariantsC, unvariants, variants2consts,
+            mapConstVs, mapConstVsC, unconstVs, consts2variants,
+            runEvalM, runEvalMWithOpts, reset, reset1, stdPredef, globals, withState,
             PredefImpl, Predef(..), ($\),
             pdCanonicalArgs, pdArity,
             normalForm, normalFlatForm,
             eval, apply, value2term, value2termM, bubble, patternMatch, vtableSelect, State(..),
             newResiduation, getMeta, setMeta, MetaState(..), variants, try,
-            evalError, evalWarn, ppValue, Choice(..), unit, poison, split, split3, split4, mapC, mapCM) where
+            evalError, evalWarn, ppValue, Choice(..), unit, poison, split, split3, split4,
+            mapC, forC, mapCM, forCM) where
 
 import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
 import GF.Infra.Ident
 import GF.Infra.CheckM
 import GF.Data.Operations(Err(..))
-import GF.Data.Utilities(maybeAt,splitAt',(<||>),anyM)
+import GF.Data.Utilities(maybeAt,splitAt',(<||>),anyM,secondM,bimapM)
 import GF.Grammar.Lookup(lookupResDef,lookupOrigInfo)
 import GF.Grammar.Grammar
 import GF.Grammar.Macros
@@ -94,17 +96,23 @@ data Value
   | VCRecType [(Label, Bool, Value)]
   | VCInts (Maybe Integer) (Maybe Integer)
 
+third f (a,b,c) = (a, b, f c)
+
 data Variants
   = VarFree [Value]
-  | VarOpts Value [(Value, Value)]
+  | VarOpts Value Value [(Value, Value, Value)]
 
 mapVariants :: (Value -> Value) -> Variants -> Variants
-mapVariants f (VarFree vs)   = VarFree (f <$> vs)
-mapVariants f (VarOpts n cs) = VarOpts n (second f <$> cs)
+mapVariants f (VarFree vs)       = VarFree (f <$> vs)
+mapVariants f (VarOpts nty n cs) = VarOpts nty n (third f <$> cs)
+
+mapVariantsC :: (Choice -> Value -> Value) -> Choice -> Variants -> Variants
+mapVariantsC f c (VarFree vs)       = VarFree (mapC f c vs)
+mapVariantsC f c (VarOpts nty n cs) = VarOpts nty n (mapC (third . f) c cs)
 
 unvariants :: Variants -> [Value]
-unvariants (VarFree vs)   = vs
-unvariants (VarOpts n cs) = snd <$> cs
+unvariants (VarFree vs)       = vs
+unvariants (VarOpts nty n cs) = cs <&> \(_,_,v) -> v
 
 isCanonicalForm :: Bool -> Value -> Bool
 isCanonicalForm flat  (VClosure {})       = True
@@ -136,15 +144,19 @@ data ConstValue a
 
 data ConstVariants a
   = ConstFree [ConstValue a]
-  | ConstOpts Value [(Value, ConstValue a)]
+  | ConstOpts Value Value [(Value, Value, ConstValue a)]
 
 mapConstVs :: (ConstValue a -> ConstValue b) -> ConstVariants a -> ConstVariants b
-mapConstVs f (ConstFree vs)   = ConstFree (f <$> vs)
-mapConstVs f (ConstOpts n cs) = ConstOpts n (second f <$> cs)
+mapConstVs f (ConstFree vs)       = ConstFree (f <$> vs)
+mapConstVs f (ConstOpts nty n cs) = ConstOpts nty n (third f <$> cs)
+
+mapConstVsC :: (Choice -> ConstValue a -> ConstValue b) -> Choice -> ConstVariants a -> ConstVariants b
+mapConstVsC f c (ConstFree vs)       = ConstFree (mapC f c vs)
+mapConstVsC f c (ConstOpts nty n cs) = ConstOpts nty n (mapC (third . f) c cs)
 
 unconstVs :: ConstVariants a -> [ConstValue a]
-unconstVs (ConstFree vs)   = vs
-unconstVs (ConstOpts n cs) = snd <$> cs
+unconstVs (ConstFree vs)       = vs
+unconstVs (ConstOpts nty n cs) = cs <&> \(_,_,v) -> v
 
 instance Functor ConstValue where
   fmap f (Const c) = Const (f c)
@@ -167,12 +179,12 @@ instance Applicative ConstValue where
   _             <*>  RunTime      = RunTime
 
 variants2consts :: (Value -> ConstValue a) -> Variants -> ConstVariants a
-variants2consts f (VarFree vs)   = ConstFree (f <$> vs)
-variants2consts f (VarOpts n os) = ConstOpts n (second f <$> os)
+variants2consts f (VarFree vs)       = ConstFree (f <$> vs)
+variants2consts f (VarOpts nty n os) = ConstOpts nty n (third f <$> os)
 
 consts2variants :: (ConstValue a -> Value) -> ConstVariants a -> Variants
-consts2variants f (ConstFree vs)   = VarFree (f <$> vs)
-consts2variants f (ConstOpts n os) = VarOpts n (second f <$> os)
+consts2variants f (ConstFree vs)       = VarFree (f <$> vs)
+consts2variants f (ConstOpts nty n os) = VarOpts nty n (third f <$> os)
 
 normalForm :: Globals -> Term -> Check Term
 normalForm g t = value2term g [] (bubble (eval g [] unit t []))
@@ -326,14 +338,17 @@ eval g env c (Markup tag as ts) [] =
                               in (VMarkup tag vas vs)
 eval g env c (Reset ctl mb_ct t qid) [] = VReset ctl (fmap (\t -> eval g env c t []) mb_ct) (eval g env c t []) qid
 eval g env c (TSymCat d r rs) []= VSymCat d r [(i,(fromJust (lookup pv env),ty)) | (i,(pv,ty)) <- rs]
-eval g env c t@(Opts n cs)  vs  = if null cs
-                                  then VError ("No options in expression:" $$ ppTerm Unqualified 0 t)
-                                  else let (c1,c2,c3) = split3 c
-                                           vn = eval g env c1 n []
-                                           vcs = mapC evalOpt c cs
-                                       in VFV c3 (VarOpts vn vcs)
-  where evalOpt c' (l,t) = let (c1,c2) = split c' in (eval g env c1 l [], eval g env c2 t vs)
-eval g env c t              vs  = VError ("Cannot reduce term" <+> pp t)
+eval g env c t@(Opts (nty,n) cs) vs = if null cs
+                                      then VError ("No options in expression:" $$ ppTerm Unqualified 0 t)
+                                      else let (c1,c2,c3) = split3 c
+                                               (c1ty,c1t) = split c1
+                                               vnty = eval g env c1ty (fromJust nty) []
+                                               vn = eval g env c1t n []
+                                               vcs = mapC evalOpt c2 cs
+                                           in VFV c3 (VarOpts vnty vn vcs)
+  where evalOpt c' ((lty,l),t) = let (c1,c2,c3) = split3 c'
+                                 in (eval g env c1 (fromJust lty) [], eval g env c2 l [], eval g env c3 t vs)
+eval g env c t vs = VError ("Cannot reduce term" <+> pp t)
 
 evalPredef :: Globals -> Choice -> Ident -> [Value] -> Value
 evalPredef g@(Gl gr pds) c n args =
@@ -381,7 +396,7 @@ apply g v                               []  = v
 
 data BubbleVariants
   = BubbleFree Int
-  | BubbleOpts Value [Value]
+  | BubbleOpts Value Value [(Value, Value)]
 
 bubble v = snd (bubble v)
   where
@@ -411,11 +426,15 @@ bubble v = snd (bubble v)
     bubble v@(VFV c (VarFree vs))
       | null vs   = (Map.empty, v)
       | otherwise = let (union,vs') = mapAccumL descend Map.empty vs
-                    in (Map.insert c (BubbleFree (length vs),1) union, addVariants (VFV c (VarFree vs')) union)
-    bubble v@(VFV c (VarOpts n os))
+                        b = BubbleFree (length vs)
+                        v' = addVariants (VFV c (VarFree vs')) union
+                    in (Map.insert c (b,1) union, v')
+    bubble v@(VFV c (VarOpts nty n os))
       | null os   = (Map.empty, v)
-      | otherwise = let (union,os') = mapAccumL (\acc (k,v) -> second (k,) $ descend acc v) Map.empty os
-                    in (Map.insert c (BubbleOpts n (fst <$> os),1) union, addVariants (VFV c (VarOpts n os')) union)
+      | otherwise = let (union,os') = mapAccumL (\acc (lty,l,v) -> second (lty,l,) $ descend acc v) Map.empty os
+                        b = BubbleOpts nty n (os <&> \(lty,l,_) -> (lty,l))
+                        v' = addVariants (VFV c (VarOpts nty n os')) union
+                    in (Map.insert c (b,1) union, v')
     bubble (VAlts v vs) = lift1L2 VAlts v vs
     bubble (VStrs vs) = liftL VStrs vs
     bubble (VMarkup tag attrs vs) =
@@ -500,8 +519,8 @@ bubble v = snd (bubble v)
       where
         addVariant c (bvs,cnt) v
           | cnt > 1   = VFV c $ case bvs of
-                                  BubbleFree k    -> VarFree (replicate k v)
-                                  BubbleOpts n os -> VarOpts n ((,v) <$> os)
+                                  BubbleFree k        -> VarFree (replicate k v)
+                                  BubbleOpts nty n os -> VarOpts nty n (os <&> \(lty,l) -> (lty,l,v))
           | otherwise = v
 
     unitfy = fmap (\(n,_) -> (n,1))
@@ -669,9 +688,10 @@ data MetaState
   | Residuation Scope (Maybe Constraint)
 data OptionInfo
   = OptionInfo
-      { optChoice  :: Choice
-      , optLabel   :: Value
-      , optChoices :: [Value]
+      { optChoice    :: Choice
+      , optLabelType :: Value
+      , optLabel     :: Value
+      , optChoices   :: [(Value, Value)]
       }
 type ChoiceMap = Map.Map Choice Int
 data State
@@ -738,6 +758,12 @@ reset (EvalM f) = EvalM $ \g k state r ws ->
     Fail   msg ws -> Fail msg ws
     Success xs ws -> k (reverse xs) state r ws
 
+reset1 :: EvalM a -> EvalM (Maybe a)
+reset1 (EvalM f) = EvalM $ \g k state r ws ->
+  case f g (\x' state x ws -> Success (x <|> Just x') ws) state Nothing ws of
+    Fail  msg ws -> Fail msg ws
+    Success x ws -> k x state r ws
+
 globals :: EvalM Globals
 globals = EvalM (\g k -> k g)
 
@@ -907,13 +933,13 @@ value2termM True xs (VFV i (VarFree vs)) = do
   v <- variants i vs
   value2termM True xs v
 value2termM False xs (VFV i (VarFree vs)) = variants' i (value2termM False xs) vs
-value2termM flat xs (VFV i (VarOpts n os)) =
+value2termM flat xs (VFV i (VarOpts nty n os)) =
   EvalM $ \g k (State choices metas opts) r msgs ->
     let j = fromMaybe 0 (Map.lookup i choices)
     in case os `maybeAt` j of
-         Just (l,t) -> case value2termM flat xs t of
-                         EvalM f -> let oi = OptionInfo i n (fst <$> os)
-                                    in f g k (State choices metas (oi:opts)) r msgs
+         Just (lty,l,t) -> case value2termM flat xs t of
+                             EvalM f -> let oi = OptionInfo i nty n (os <&> \(lty,l,_) -> (lty,l))
+                                        in f g k (State choices metas (oi:opts)) r msgs
          Nothing    -> Fail ("Index" <+> j <+> "out of bounds for option:" $$ ppValue Unqualified 0 n) msgs
 value2termM flat xs (VPatt min max p) = return (EPatt min max p)
 value2termM flat xs (VPattType v) = do t <- value2termM flat xs v
@@ -1020,7 +1046,9 @@ ppValue q d (VC v1 v2) = prec d 1 (hang (ppValue q 2 v1) 2 ("++" <+> ppValue q 1
 ppValue q d (VGlue v1 v2) = prec d 2 (ppValue q 3 v1 <+> '+'  <+> ppValue q 2 v2)
 ppValue q d (VPatt _ _ _) = pp "VPatt"
 ppValue q d (VPattType _) = pp "VPattType"
-ppValue q d (VFV i vs) = prec d 4 ("variants" <+> pp i <+> braces (fsep (punctuate ';' (map (ppValue q 0) (unvariants vs)))))
+ppValue q d (VFV i (VarFree vs)) = prec d 4 ("variants" <+> pp i <+> braces (fsep (punctuate ';' (map (ppValue q 0) vs))))
+ppValue q d (VFV i (VarOpts _ n os)) = prec d 4 ("option" <+> ppValue q 0 n <+> "of" <+> pp i <+> braces (fsep (punctuate ';'
+                                                  (map (\(_,l,v) -> parens (ppValue q 0 l) <+> "=>" <+> ppValue q 0 v) os))))
 ppValue q d (VAlts e xs) = prec d 4 ("pre" <+> braces (ppValue q 0 e <> ';' <+> fsep (punctuate ';' (map (ppAltern q) xs))))
 ppValue q d (VStrs _) = pp "VStrs"
 ppValue q d (VMarkup _ _ _) = pp "VMarkup"
@@ -1129,6 +1157,9 @@ mapC f c (x:xs) =
   let (!c1,!c2) = split c
   in f c1 x : mapC f c2 xs
 
+forC :: Choice -> [a] -> (Choice -> a -> b) -> [b]
+forC c xs f = mapC f c xs
+
 mapCM :: Monad m => (Choice -> a -> m b) -> Choice -> [a] -> m [b]
 mapCM f c []     = return []
 mapCM f c [x]    = do y <- f c x
@@ -1138,3 +1169,6 @@ mapCM f c (x:xs) = do
   y  <- f c1 x
   ys <- mapCM f c2 xs
   return (y:ys)
+
+forCM :: Monad m => Choice -> [a] -> (Choice -> a -> m b) -> m [b]
+forCM c xs f = mapCM f c xs
diff --git a/src/compiler/api/GF/Compile/Repl.hs b/src/compiler/api/GF/Compile/Repl.hs
index 8cb7d92a0..066ee1dc1 100644
--- a/src/compiler/api/GF/Compile/Repl.hs
+++ b/src/compiler/api/GF/Compile/Repl.hs
@@ -23,6 +23,7 @@ import GF.Compile.Compute.Concrete2
   , ChoiceMap
   , Globals(Gl)
   , OptionInfo(..)
+  , bubble
   , stdPredef
   , unit
   , eval
@@ -57,7 +58,6 @@ import GF.Infra.Ident (moduleNameS)
 import GF.Infra.Option (noOptions)
 import GF.Infra.UseIO (justModuleName)
 import GF.Text.Pretty (render)
-import Debug.Trace
 
 data ReplOpts = ReplOpts
   { lang :: Lang
@@ -282,11 +282,11 @@ runRepl' opts@ReplOpts { lang, evalToFlat } gl@(Gl g _) = do
         outputStrLn $ show i ++ (if null opts then ". " else "*. ") ++ render (ppTerm Unqualified 0 r)
     
     outputOptions ois os =
-      forM_ ois $ \(OptionInfo c n ls) -> do
+      forM_ ois $ \(OptionInfo c _ n ls) -> do
         outputStrLn ""
         outputStrLn $ show (unchoice c) ++ ") " ++ render (ppValue Unqualified 0 n)
         let sel = fromMaybe 0 (Map.lookup c os) + 1
-        forM_ (zip [1..] ls) $ \(i, l) ->
+        forM_ (zip [1..] ls) $ \(i, (_,l)) ->
           outputStrLn $ (if i == sel then "->" else "  ") ++ show i ++ ". " ++ render (ppValue Unqualified 0 l)
 
 runRepl :: ReplOpts -> IO ()
diff --git a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs
index 90ddfa3bd..2c03d866f 100644
--- a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs
+++ b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs
@@ -407,12 +407,17 @@ tcRho scope c (Reset ctl mb_ct t qid) mb_ty
            VApp c qid [] -> return (Reset ctl mb_ct t qid, ty)
            _             -> evalError (pp "Needs atomic type"<+>ppValue Unqualified 0 ty)
   | otherwise = evalError (pp "Operator" <+> pp ctl <+> pp "is not defined")
-tcRho scope s (Opts n cs) mb_ty = do
+tcRho scope s (Opts (nty,n) cs) mb_ty = do
+  gl <- globals
   let (s1,s2,s3) = split3 s
-  (n,_) <- tcRho scope s1 n Nothing
-  (ls,_) <- tcUnifying scope s2 (fst <$> cs) Nothing
+  (n,nty) <- tcRho scope s1 n (nty <&> \ty -> eval gl [] poison ty [])
+  nty <- value2termM True [] nty
+  ls <- forCM s2 cs $ \s' ((lty,l),_) -> do
+    (l,lty) <- tcRho scope s' l (lty <&> \ty -> eval gl [] poison ty [])
+    lty <- value2termM True [] lty
+    return (Just lty, l)
   (ts,ty) <- tcUnifying scope s3 (snd <$> cs) mb_ty
-  return (Opts n (zip ls ts), ty)
+  return (Opts (Just nty, n) (zip ls ts), ty)
 tcRho scope s t _ = unimplemented ("tcRho "++show t)
 
 evalCodomain :: Scope -> Ident -> Value -> EvalM Value
@@ -1179,9 +1184,9 @@ quantify scope t tvs ty = do
     check m n xs (VFV c (VarFree vs)) = do
       (xs,vs) <- mapAccumM (check m n) xs vs
       return (xs,VFV c (VarFree vs))
-    check m n xs (VFV c (VarOpts name os)) = do
-      (xs,os) <- mapAccumM (\acc (l,v) -> second (l,) <$> check m n acc v) xs os
-      return (xs,VFV c (VarOpts name os))
+    check m n xs (VFV c (VarOpts nty name os)) = do
+      (xs,os) <- mapAccumM (\acc (lty,l,v) -> second (lty,l,) <$> check m n acc v) xs os
+      return (xs,VFV c (VarOpts nty name os))
     check m n xs (VAlts v vs)      = do
       (xs,v)  <- check m n xs v
       (xs,vs) <- mapAccumM (\xs (v1,v2) -> do (xs,v1) <- check m n xs v1
diff --git a/src/compiler/api/GF/Data/Utilities.hs b/src/compiler/api/GF/Data/Utilities.hs
index f8d76dd28..fbb309f44 100644
--- a/src/compiler/api/GF/Data/Utilities.hs
+++ b/src/compiler/api/GF/Data/Utilities.hs
@@ -11,13 +11,13 @@
 -- Basic functions not in the standard libraries
 -----------------------------------------------------------------------------
 
-
+{-# LANGUAGE TupleSections #-}
 module GF.Data.Utilities(module GF.Data.Utilities) where
 
 import Data.Bifunctor (first)
 import Data.Maybe
 import Data.List
-import Control.Monad (MonadPlus(..),foldM,liftM,when)
+import Control.Monad (MonadPlus(..),foldM,liftM,liftM2,when)
 import Control.Applicative(liftA2)
 import qualified Data.Set as Set
 
@@ -128,7 +128,7 @@ compareBy f = both f compare
 both :: (a -> b) -> (b -> b -> c) -> a -> a -> c
 both f g x y = g (f x) (f y)
 
--- * functions on pairs
+-- * functions on tuples
 
 apFst :: (a -> a') -> (a, b) -> (a', b)
 apFst f (a, b) = (f a, b)
@@ -174,6 +174,18 @@ allM p = foldM (\b x -> if b then p x else return False) True
 anyM :: (Foldable f, Monad m) => (a -> m Bool) -> f a -> m Bool
 anyM p = foldM (\b x -> if b then return True else p x) False
 
+-- | Lifts a monadic action to pairs in the first element.
+firstM :: Monad m => (a -> m a') -> (a, b) -> m (a', b)
+firstM f (a, b) = (,b) <$> f a
+
+-- | Lifts a monadic action to pairs in the second element.
+secondM :: Monad m => (b -> m b') -> (a, b) -> m (a, b')
+secondM f (a, b) = (a,) <$> f b
+
+-- | Lifts a pair of monadic actions to an action on pairs, sequencing left-to-right.
+bimapM :: Monad m => (a -> m a') -> (b -> m b') -> (a, b) -> m (a', b')
+bimapM f g (a, b) = liftM2 (,) (f a) (g b)
+
 -- * functions on Maybes
 
 -- | Returns the argument on the right, or a default value on the left.
diff --git a/src/compiler/api/GF/Grammar/Grammar.hs b/src/compiler/api/GF/Grammar/Grammar.hs
index 0300b19a8..dda33193d 100644
--- a/src/compiler/api/GF/Grammar/Grammar.hs
+++ b/src/compiler/api/GF/Grammar/Grammar.hs
@@ -343,9 +343,10 @@ data Info =
  | AnyInd Bool ModuleName                        -- ^ (/INDIR/) the 'Bool' says if canonical
   deriving Show
 
-type Type = Term
-type Cat  = QIdent
-type Fun  = QIdent
+type Type    = Term
+type MTyTerm = (Maybe Term, Term)
+type Cat     = QIdent
+type Fun     = QIdent
 
 type QIdent = (ModuleName,Ident)
 
@@ -373,7 +374,7 @@ data Term =
  | P Term Label                  -- ^ projection:  @r.p@
  | ExtR Term Term                -- ^ extension:   @R ** {x : A}@ (both types and terms)
 
- | Opts Term [Option]            -- ^ options:     @options s in { e => x ; ... }@
+ | Opts MTyTerm [Option]         -- ^ options:     @options s in { e => x ; ... }@
 
  | Table Term Term               -- ^ table type:  @P => A@
  | T TInfo [Case]                -- ^ table:       @table {p => c ; ...}@
@@ -466,7 +467,7 @@ type Equation = ([Patt],Term)
 
 type Labelling = (Label, Type) 
 type Assign = (Label, (Maybe Type, Term)) 
-type Option = (Term, Term)
+type Option = (MTyTerm, Term)
 type Case = (Patt, Term) 
 --type Cases = ([Patt], Term) 
 type LocalDef = (Ident, (Maybe Type, Term))
diff --git a/src/compiler/api/GF/Grammar/Parser.y b/src/compiler/api/GF/Grammar/Parser.y
index c81724d24..3e6cdfac3 100644
--- a/src/compiler/api/GF/Grammar/Parser.y
+++ b/src/compiler/api/GF/Grammar/Parser.y
@@ -452,7 +452,7 @@ Exp4 :: { Term }
 Exp4
   : Exp4 Exp5                        { App $1 $2 }
   | Exp4 '{' Exp '}'                 { App $1 (ImplArg $3) } 
-  | 'option' Exp 'of' '{' ListOpt '}' { Opts $2 $5 }
+  | 'option' Exp 'of' '{' ListOpt '}' { Opts (Nothing, $2) $5 }
   | 'case' Exp 'of' '{' ListCase '}' { let annot = case $2 of
                                              Typed _ t -> TTyped t
                                              _         -> TRaw
@@ -611,7 +611,7 @@ ListPattTupleComp
 
 Opt :: { Option }
 Opt
-  : '(' Exp ')' '=>' Exp { ($2,$5) }
+  : '(' Exp ')' '=>' Exp { ((Nothing,$2),$5) }
 
 ListOpt :: { [Option] }
 ListOpt
diff --git a/src/compiler/api/GF/Grammar/Printer.hs b/src/compiler/api/GF/Grammar/Printer.hs
index 3f7364bbb..d58f19e66 100644
--- a/src/compiler/api/GF/Grammar/Printer.hs
+++ b/src/compiler/api/GF/Grammar/Printer.hs
@@ -219,6 +219,8 @@ ppTerm q d (S x y)     = case x of
 ppTerm q d (ExtR x y)  = prec d 3 (ppTerm q 3 x <+> "**" <+> ppTerm q 4 y)
 ppTerm q d (App x y)   = prec d 4 (ppTerm q 4 x <+> ppTerm q 5 y)
 ppTerm q d (V e es)    = hang "table" 2 (sep [ppTerm q 6 e,brackets (fsep (punctuate ';' (map (ppTerm q 0) es)))])
+ppTerm q d (Opts (_,n) cs) = prec d 4 ("option" <+> ppTerm q 0 n <+> "of" <+> braces (fsep (punctuate ';'
+                                        (map (\((_,l),t) -> parens (ppTerm q 0 l) <+> "=>" <+> ppTerm q 0 t) cs))))
 ppTerm q d (FV es)     = prec d 4 ("variants" <+> braces (fsep (punctuate ';' (map (ppTerm q 0) es))))
 ppTerm q d (AdHocOverload es)     = "overload" <+> braces (fsep (punctuate ';' (map (ppTerm q 0) es)))
 ppTerm q d (Alts e xs) = prec d 4 ("pre" <+> braces (ppTerm q 0 e <> ';' <+> fsep (punctuate ';' (map (ppAltern q) xs))))