diff --git a/examples/primitives-documentation.golden b/examples/primitives-documentation.golden
index f92ed433..740067ae 100644
--- a/examples/primitives-documentation.golden
+++ b/examples/primitives-documentation.golden
@@ -39,6 +39,7 @@
 (type) : Problem
 (pattern) : Problem
 (type-pattern) : Problem
+(type-constructor) : Problem
 (nothing) : ∀(α : *). (Maybe α)
 (nil) : ∀(α : *). (List α)
 make-introducer : (Macro (ScopeAction → (Syntax → Syntax)))
diff --git a/examples/primitives-documentation.kl b/examples/primitives-documentation.kl
index e171033b..e9cf547f 100644
--- a/examples/primitives-documentation.kl
+++ b/examples/primitives-documentation.kl
@@ -125,6 +125,7 @@
 -- expression : Type -> Problem
 (example (pattern))
 (example (type-pattern))
+(example (type-constructor))
 --
 -- Maybe : Type -> Type
 (example nothing)
diff --git a/src/Binding.hs b/src/Binding.hs
index 25bf4104..b283d2aa 100644
--- a/src/Binding.hs
+++ b/src/Binding.hs
@@ -16,7 +16,6 @@ import Data.Sequence (Seq)
 
 import Binding.Info
 import Phase
-import ShortShow
 import Syntax.SrcLoc
 import Unique
 
@@ -35,9 +34,6 @@ instance HasKey Binding where
 instance Show Binding where
   show (Binding b) = "(Binding " ++ show (hashUnique b) ++ ")"
 
-instance ShortShow Binding where
-  shortShow (Binding b) = "b" ++ show (hashUnique b)
-
 newtype BindingTable = BindingTable { _bindings :: HashMap Text (Seq (ScopeSet, Binding, BindingInfo SrcLoc)) }
   deriving (Data, Show)
 makeLenses ''BindingTable
diff --git a/src/Binding/Info.hs b/src/Binding/Info.hs
index bcd5fc8d..bfee3176 100644
--- a/src/Binding/Info.hs
+++ b/src/Binding/Info.hs
@@ -4,8 +4,6 @@ module Binding.Info where
 
 import Data.Data (Data)
 
-import ShortShow
-
 data BindingInfo loc
   = BoundLocally loc
   | Defined loc
@@ -13,8 +11,3 @@ data BindingInfo loc
   -- enable go to definition
   | Imported loc
   deriving (Data, Eq, Functor, Show)
-
-instance ShortShow loc => ShortShow (BindingInfo loc) where
-  shortShow (BoundLocally l) = "BoundLocally " ++ shortShow l
-  shortShow (Defined l) = "Defined " ++ shortShow l
-  shortShow (Imported l) = "Imported " ++ shortShow l
diff --git a/src/Core.hs b/src/Core.hs
index ece6aff9..37ef8fd0 100644
--- a/src/Core.hs
+++ b/src/Core.hs
@@ -31,7 +31,6 @@ import Alpha
 import Datatype
 import ModuleName
 import Phase
-import ShortShow
 import Syntax
 import Syntax.SrcLoc
 import Type
@@ -73,26 +72,26 @@ instance Show MacroVar where
   show (MacroVar i) = "(MacroVar " ++ show (hashUnique i) ++ ")"
 
 data TypePattern
-  = TypePattern (TyF (Ident, Var))
-  | AnyType Ident Var
+  = TypeCtorPattern (TyF (Ident, Var))
+  | TypePatternVar Ident Var
   deriving (Data, Eq, Show)
 
-data ConstructorPatternF pat
-  = CtorPattern !Constructor [pat]
+data DataPatternF pat
+  = DataCtorPattern !Constructor [pat]
   | PatternVar Ident Var
   deriving (Data, Eq, Foldable, Functor, Show, Traversable)
-makePrisms ''ConstructorPatternF
+makePrisms ''DataPatternF
 
-newtype ConstructorPattern =
-  ConstructorPattern { unConstructorPattern :: ConstructorPatternF ConstructorPattern }
+newtype DataPattern =
+  DataPattern { unDataPattern :: DataPatternF DataPattern }
   deriving (Data, Eq, Show)
-makePrisms ''ConstructorPattern
+makePrisms ''DataPattern
 
-instance Phased a => Phased (ConstructorPatternF a) where
+instance Phased a => Phased (DataPatternF a) where
   shift i = fmap (shift i)
 
-instance Phased ConstructorPattern where
-  shift i = over _ConstructorPattern (shift i)
+instance Phased DataPattern where
+  shift i = over _DataPattern (shift i)
 
 instance Phased TypePattern where
   shift _ = id
@@ -316,7 +315,7 @@ instance (Phased typePat, Phased pat, Phased core) => Phased (CoreF typePat pat
 
 -- | A fully-expanded expression, ready to be evaluated.
 newtype Core = Core
-  { unCore :: CoreF TypePattern ConstructorPattern Core }
+  { unCore :: CoreF TypePattern DataPattern Core }
   deriving (Data, Eq, Show)
 makePrisms ''Core
 
@@ -386,13 +385,13 @@ instance (AlphaEq typePat, AlphaEq pat, AlphaEq core) => AlphaEq (CoreF typePat
   alphaCheck _ _ = notAlphaEquivalent
 
 
-instance AlphaEq ConstructorPattern where
+instance AlphaEq DataPattern where
   alphaCheck p1 p2 =
-    alphaCheck (unConstructorPattern p1) (unConstructorPattern p2)
+    alphaCheck (unDataPattern p1) (unDataPattern p2)
 
-instance AlphaEq a => AlphaEq (ConstructorPatternF a) where
-  alphaCheck (CtorPattern c1 vars1)
-             (CtorPattern c2 vars2) = do
+instance AlphaEq a => AlphaEq (DataPatternF a) where
+  alphaCheck (DataCtorPattern c1 vars1)
+             (DataCtorPattern c2 vars2) = do
     alphaCheck c1 c2
     for_ (zip vars1 vars2) (uncurry alphaCheck)
   alphaCheck (PatternVar _ x1)
@@ -401,11 +400,11 @@ instance AlphaEq a => AlphaEq (ConstructorPatternF a) where
   alphaCheck _ _ = notAlphaEquivalent
 
 instance AlphaEq TypePattern where
-  alphaCheck (TypePattern t1)
-             (TypePattern t2) =
+  alphaCheck (TypeCtorPattern t1)
+             (TypeCtorPattern t2) =
     alphaCheck t1 t2
-  alphaCheck (AnyType _ x1)
-             (AnyType _ x2) =
+  alphaCheck (TypePatternVar _ x1)
+             (TypePatternVar _ x2) =
     alphaCheck x1 x2
   alphaCheck _ _ = notAlphaEquivalent
 
@@ -453,227 +452,3 @@ instance AlphaEq core => AlphaEq (ScopedList core) where
              (ScopedList elements2 scope2) = do
     alphaCheck elements1 elements2
     alphaCheck scope1    scope2
-
-
-instance ShortShow a => ShortShow (SyntaxError a) where
-  shortShow (SyntaxError locations message)
-    = "(SyntaxError "
-   ++ shortShow locations
-   ++ " "
-   ++ shortShow message
-   ++ ")"
-
-instance ShortShow Var where
-  shortShow (Var x) = shortShow x
-
-instance (ShortShow typePat, ShortShow pat, ShortShow core) =>
-         ShortShow (CoreF typePat pat core) where
-  shortShow (CoreVar var)
-    = "(Var "
-   ++ shortShow var
-   ++ ")"
-  shortShow (CoreLet _ x def body)
-    = "(Let "
-   ++ shortShow x
-   ++ " "
-   ++ shortShow def
-   ++ " "
-   ++ shortShow body
-   ++ ")"
-  shortShow (CoreLetFun _ f _ x def body)
-    = "(LetFun "
-   ++ shortShow f
-   ++ " "
-   ++ shortShow x
-   ++ " "
-   ++ shortShow def
-   ++ " "
-   ++ shortShow body
-   ++ ")"
-  shortShow (CoreLam _ x body)
-    = "(Lam "
-   ++ shortShow x
-   ++ " "
-   ++ shortShow body
-   ++ ")"
-  shortShow (CoreApp fun arg)
-    = "(App "
-   ++ shortShow fun
-   ++ " "
-   ++ shortShow arg
-   ++ ")"
-  shortShow (CoreCtor ctor args)
-    = "(Ctor "
-   ++ shortShow ctor
-   ++ " "
-   ++ shortShow args
-   ++ ")"
-  shortShow (CoreDataCase _ scrut cases)
-    = "(DataCase "
-   ++ shortShow scrut
-   ++ " "
-   ++ intercalate ", " (map shortShow cases)
-   ++ ")"
-  shortShow (CoreInteger i)
-    = show i
-  shortShow (CoreString str)
-    = "(String " ++ show str ++ ")"
-  shortShow (CoreError what)
-    = "(Error "
-   ++ shortShow what
-   ++ ")"
-  shortShow (CorePureMacro x)
-    = "(PureMacro "
-   ++ shortShow x
-   ++ ")"
-  shortShow (CoreBindMacro hd tl)
-    = "(BindMacro "
-   ++ shortShow hd
-   ++ " "
-   ++ shortShow tl
-   ++ ")"
-  shortShow (CoreSyntaxError syntaxError)
-    = "(SyntaxError "
-   ++ shortShow syntaxError
-   ++ ")"
-  shortShow (CoreIdentEq how e1 e2)
-    = "(CoreIdentEq " ++ show how
-    ++ " " ++ shortShow e1
-    ++ " " ++ shortShow e2 ++ ")"
-  shortShow (CoreLog msg)
-    = "(CoreLog " ++ shortShow msg ++ ")"
-  shortShow CoreMakeIntroducer
-    = "(CoreMakeIntroducer)"
-  shortShow CoreWhichProblem
-    = "(CoreWhichProblem)"
-  shortShow (CoreSyntax syntax)
-    = "(Syntax "
-   ++ shortShow syntax
-   ++ ")"
-  shortShow (CoreCase _ scrutinee cases)
-    = "(Case "
-   ++ shortShow scrutinee
-   ++ " "
-   ++ shortShow cases
-   ++ ")"
-  shortShow (CoreIdent scopedIdent)
-    = "(Ident "
-   ++ shortShow scopedIdent
-   ++ ")"
-  shortShow (CoreEmpty scopedEmpty)
-    = "(Empty "
-   ++ shortShow scopedEmpty
-   ++ ")"
-  shortShow (CoreCons scopedCons)
-    = "(Cons "
-   ++ shortShow scopedCons
-   ++ ")"
-  shortShow (CoreList scopedVec)
-    = "(List "
-   ++ shortShow scopedVec
-   ++ ")"
-  shortShow (CoreIntegerSyntax scopedStr)
-    = "(IntegerSyntax "
-   ++ shortShow scopedStr
-   ++ ")"
-  shortShow (CoreStringSyntax scopedStr)
-    = "(StringSyntax "
-   ++ shortShow scopedStr
-   ++ ")"
-  shortShow (CoreReplaceLoc loc stx)
-    = "(ReplaceLoc "
-   ++ shortShow loc ++ " "
-   ++ shortShow stx ++ ")"
-  shortShow (CoreTypeCase _ scrut pats)
-    = "(TypeCase "
-   ++ shortShow scrut
-   ++ " "
-   ++ intercalate ", " (map shortShow pats)
-   ++ ")"
-
-
-instance ShortShow Core where
-  shortShow (Core x) = shortShow x
-
-instance ShortShow ConstructorPattern where
-  shortShow = shortShow . unConstructorPattern
-
-instance ShortShow a => ShortShow (ConstructorPatternF a) where
-  shortShow (CtorPattern ctor vars) =
-    "(" ++ shortShow ctor ++
-    " " ++ intercalate " " (map shortShow vars) ++
-    ")"
-  shortShow (PatternVar ident _var) =
-    "(PatternVar " ++ shortShow ident ++ " )"
-
-instance ShortShow TypePattern where
-  shortShow (TypePattern t) =
-    "(" ++ shortShow (fmap fst t) ++ ")"
-  shortShow (AnyType ident _var) =
-    "(AnyConstructor " ++ shortShow ident ++ " )"
-
-
-instance ShortShow SyntaxPattern where
-  shortShow (SyntaxPatternIdentifier _ x) = shortShow x
-  shortShow (SyntaxPatternInteger _ x) = "(Integer " ++ shortShow x ++ ")"
-  shortShow (SyntaxPatternString _ x) = "(String " ++ shortShow x ++ ")"
-  shortShow SyntaxPatternEmpty = "Empty"
-  shortShow (SyntaxPatternCons _ x _ xs)
-    = "(Cons "
-   ++ shortShow x
-   ++ " "
-   ++ shortShow xs
-   ++ ")"
-  shortShow (SyntaxPatternList xs)
-    = "(List "
-   ++ shortShow (map snd xs)
-   ++ ")"
-  shortShow SyntaxPatternAny = "_"
-
-instance ShortShow core => ShortShow (ScopedIdent core) where
-  shortShow (ScopedIdent ident scope)
-    = "(ScopedIdent "
-   ++ shortShow ident
-   ++ " "
-   ++ shortShow scope
-   ++ ")"
-
-instance ShortShow core => ShortShow (ScopedEmpty core) where
-  shortShow (ScopedEmpty scope)
-    = "(ScopedEmpty "
-   ++ shortShow scope
-   ++ ")"
-
-instance ShortShow core => ShortShow (ScopedCons core) where
-  shortShow (ScopedCons hd tl scope)
-    = "(ScopedCons "
-   ++ shortShow hd
-   ++ " "
-   ++ shortShow tl
-   ++ " "
-   ++ shortShow scope
-   ++ ")"
-
-instance ShortShow core => ShortShow (ScopedList core) where
-  shortShow (ScopedList elements scope)
-    = "(ScopedList "
-   ++ shortShow elements
-   ++ " "
-   ++ shortShow scope
-   ++ ")"
-
-instance ShortShow core => ShortShow (ScopedInteger core) where
-  shortShow (ScopedInteger str scope)
-    = "(ScopedInteger "
-   ++ shortShow str
-   ++ " "
-   ++ shortShow scope
-   ++ ")"
-
-instance ShortShow core => ShortShow (ScopedString core) where
-  shortShow (ScopedString str scope)
-    = "(ScopedString "
-   ++ shortShow str
-   ++ " "
-   ++ shortShow scope
-   ++ ")"
diff --git a/src/Datatype.hs b/src/Datatype.hs
index a54d1c0e..4cf110aa 100644
--- a/src/Datatype.hs
+++ b/src/Datatype.hs
@@ -14,7 +14,6 @@ import Data.Hashable
 import Alpha
 import Kind
 import ModuleName
-import ShortShow
 import GHC.Generics (Generic)
 
 newtype DatatypeName = DatatypeName { _datatypeNameText :: Text }
@@ -46,8 +45,6 @@ data Constructor
 makeLenses ''Constructor
 
 instance Hashable Constructor
-instance ShortShow Constructor where
-  shortShow = show
 
 instance AlphaEq Constructor where
   alphaCheck c1 c2
diff --git a/src/Evaluator.hs b/src/Evaluator.hs
index d5aa114c..5a1a3f8d 100644
--- a/src/Evaluator.hs
+++ b/src/Evaluator.hs
@@ -17,7 +17,6 @@ import qualified Data.Text as T
 
 import Core
 import Env
-import ShortShow
 import Syntax
 import Syntax.SrcLoc
 import Type
@@ -41,16 +40,6 @@ data EvalError
   deriving (Show)
 makePrisms ''EvalError
 
-evalErrorText :: EvalError -> Text
-evalErrorText (EvalErrorUnbound x) = "Unbound: " <> T.pack (show x)
-evalErrorText (EvalErrorType (TypeError expected got)) =
-  "Wrong type. Expected a " <> expected <> " but got a " <> got
-evalErrorText (EvalErrorCase loc val) =
-  "Didn't match any pattern at " <> T.pack (shortShow loc) <> ": " <> valueText val
-evalErrorText (EvalErrorUser what) =
-  T.pack (shortShow (stxLoc what)) <> ":\n\t" <>
-  syntaxText what
-
 newtype Eval a = Eval
    { runEval :: ReaderT VEnv (ExceptT EvalError IO) a }
    deriving (Functor, Applicative, Monad,
@@ -273,24 +262,24 @@ withScopeOf scope expr = do
     Syntax (Stx scopeSet loc _) ->
       pure $ ValueSyntax $ Syntax $ Stx scopeSet loc expr
 
-doDataCase :: SrcLoc -> Value -> [(ConstructorPattern, Core)] -> Eval Value
+doDataCase :: SrcLoc -> Value -> [(DataPattern, Core)] -> Eval Value
 doDataCase loc v0 [] = throwError (EvalErrorCase loc v0)
 doDataCase loc v0 ((pat, rhs) : ps) =
-  match (doDataCase loc v0 ps) (eval rhs) [(unConstructorPattern pat, v0)]
+  match (doDataCase loc v0 ps) (eval rhs) [(unDataPattern pat, v0)]
   where
     match ::
       Eval Value {- ^ Failure continuation -} ->
       Eval Value {- ^ Success continuation, to be used in an extended environment -} ->
-      [(ConstructorPatternF ConstructorPattern, Value)] {- ^ Subpatterns and their scrutinees -} ->
+      [(DataPatternF DataPattern, Value)] {- ^ Subpatterns and their scrutinees -} ->
       Eval Value
     match _fk sk [] = sk
-    match fk sk ((CtorPattern ctor subPats, tgt) : more) =
+    match fk sk ((DataCtorPattern ctor subPats, tgt) : more) =
       case tgt of
         ValueCtor c args
           | c == ctor ->
             if length subPats /= length args
               then error $ "Type checker bug: wrong number of pattern vars for constructor " ++ show c
-              else match fk sk (zip (map unConstructorPattern subPats) args ++ more)
+              else match fk sk (zip (map unDataPattern subPats) args ++ more)
         _otherValue -> fk
     match fk sk ((PatternVar n x, tgt) : more) =
       match fk (withExtendedEnv n x tgt $ sk) more
@@ -300,7 +289,7 @@ doTypeCase blameLoc v0 [] = throwError (EvalErrorCase blameLoc (ValueType v0))
 doTypeCase blameLoc (Ty v0) ((p, rhs0) : ps) = match (doTypeCase blameLoc (Ty v0) ps) p rhs0 v0
   where
     match :: Eval Value -> TypePattern -> Core -> TyF Ty -> Eval Value
-    match next (TypePattern t) rhs scrut =
+    match next (TypeCtorPattern t) rhs scrut =
       case (t, scrut) of
         -- unification variables never match; instead, type-case remains stuck
         -- until the variable is unified with a concrete type constructor or a
@@ -315,7 +304,7 @@ doTypeCase blameLoc (Ty v0) ((p, rhs0) : ps) = match (doTypeCase blameLoc (Ty v0
                                 | arg <- args2]
                                 (eval rhs)
         (_, _) -> next
-    match _next (AnyType n x) rhs scrut =
+    match _next (TypePatternVar n x) rhs scrut =
       withExtendedEnv n x (ValueType (Ty scrut)) (eval rhs)
 
 doCase :: SrcLoc -> Value -> [(SyntaxPattern, Core)] -> Eval Value
diff --git a/src/Expander.hs b/src/Expander.hs
index ff581681..4862a931 100644
--- a/src/Expander.hs
+++ b/src/Expander.hs
@@ -13,6 +13,7 @@
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE ViewPatterns #-}
+{-# OPTIONS -Wno-incomplete-uni-patterns #-}
 module Expander (
   -- * Concrete expanders
     expandExpr
@@ -51,6 +52,7 @@ import Control.Monad.Trans.State.Strict (StateT, execStateT, modify', runStateT)
 import Data.Foldable
 import Data.Function (on)
 import Data.List (nub)
+import Data.List.NonEmpty (NonEmpty((:|)))
 import qualified Data.HashMap.Strict as HM
 import Data.Maybe
 import Data.Sequence (Seq(..))
@@ -79,7 +81,6 @@ import Parser
 import Phase
 import Pretty
 import ScopeSet (ScopeSet)
-import ShortShow
 import SplitCore
 import SplitType
 import Syntax
@@ -387,9 +388,11 @@ initializeKernel outputChannel = do
   traverse_ (uncurry addDeclPrimitive) declPrims
   traverse_ (uncurry addTypePrimitive) typePrims
   traverse_ (uncurry addPatternPrimitive) patternPrims
+  traverse_ (uncurry addTypePatternPrimitive) typePatternPrims
+  traverse_ (uncurry addTypeCtorPrimitive) typeCtorPrims
+  traverse_ (uncurry addPolyProblemPrimitive) polyProblemPrims
   traverse_ addDatatypePrimitive datatypePrims
   traverse_ addFunPrimitive funPrims
-  addUniversalPrimitive "with-unknown-type" Prims.makeLocalType
 
 
   where
@@ -595,7 +598,15 @@ initializeKernel outputChannel = do
       [ ("ScopeAction", [], [("flip", []), ("add", []), ("remove", [])])
       , ("Unit", [], [("unit", [])])
       , ("Bool", [], [("true", []), ("false", [])])
-      , ("Problem", [], [("module", []), ("declaration", []), ("type", []), ("expression", [tType]), ("pattern", []), ("type-pattern", [])])
+      , ("Problem", [],
+          [ ("module", [])
+          , ("declaration", [])
+          , ("type", [])
+          , ("expression", [tType])
+          , ("pattern", [])
+          , ("type-pattern", [])
+          , ("type-constructor", [])
+          ])
       , ("Maybe", [KStar], [("nothing", []), ("just", [tSchemaVar 0 []])])
       , ("List"
         , [KStar]
@@ -615,10 +626,10 @@ initializeKernel outputChannel = do
         )
       ]
 
-    modPrims :: [(Text, DeclTreePtr -> Syntax -> Expand ())]
+    modPrims :: [(Text, Prims.ModulePrim)]
     modPrims = [("#%module", Prims.makeModule expandDeclForms)]
 
-    declPrims :: [(Text, DeclTreePtr -> DeclOutputScopesPtr -> Syntax -> Expand ())]
+    declPrims :: [(Text, Prims.DeclPrim)]
     declPrims =
       [ ("define", Prims.define)
       , ("datatype", Prims.datatype)
@@ -631,7 +642,7 @@ initializeKernel outputChannel = do
       , ("group", Prims.group expandDeclForms)
       ]
 
-    exprPrims :: [(Text, Ty -> SplitCorePtr -> Syntax -> Expand ())]
+    exprPrims :: [(Text, Prims.ExprPrim)]
     exprPrims =
       [ ("error", Prims.err)
       , ("the", Prims.the)
@@ -663,8 +674,20 @@ initializeKernel outputChannel = do
       , ("type-case", Prims.typeCase)
       ]
 
-    patternPrims :: [(Text, Either (Ty, PatternPtr) TypePatternPtr -> Syntax -> Expand ())]
-    patternPrims = [("else", Prims.elsePattern)]
+    patternPrims :: [(Text, Prims.PatternPrim)]
+    patternPrims = []
+
+    typePatternPrims :: [(Text, Prims.TypePatternPrim)]
+    typePatternPrims = []
+
+    typeCtorPrims :: [(Text, Prims.TypeCtorPrim)]
+    typeCtorPrims = []
+
+    polyProblemPrims :: [(Text, Prims.PolyProblemPrim)]
+    polyProblemPrims =
+      [ ("else", Prims.elsePattern)
+      , ("with-unknown-type", Prims.makeLocalType)
+      ]
 
     addToKernel name p b =
       modifyState $ over expanderKernelExports $ addExport p name b
@@ -722,13 +745,29 @@ initializeKernel outputChannel = do
 
 
     addPatternPrimitive ::
-      Text -> (Either (Ty, PatternPtr) TypePatternPtr -> Syntax -> Expand ()) -> Expand ()
+      Text -> (Ty -> PatternPtr -> Syntax -> Expand ()) -> Expand ()
     addPatternPrimitive name impl = do
       let val = EPrimPatternMacro impl
       b <- freshBinding
       bind b val
       addToKernel name runtime b
 
+    addTypePatternPrimitive ::
+      Text -> (TypePatternPtr -> Syntax -> Expand ()) -> Expand ()
+    addTypePatternPrimitive name impl = do
+      let val = EPrimTypePatternMacro impl
+      b <- freshBinding
+      bind b val
+      addToKernel name runtime b
+
+    addTypeCtorPrimitive ::
+      Text -> (TypeCtorPtr -> Syntax -> Expand ()) -> Expand ()
+    addTypeCtorPrimitive name impl = do
+      let val = EPrimTypeCtorMacro impl
+      b <- freshBinding
+      bind b val
+      addToKernel name runtime b
+
     addModulePrimitive :: Text -> (DeclTreePtr -> Syntax -> Expand ()) -> Expand ()
     addModulePrimitive name impl = do
       let val = EPrimModuleMacro impl
@@ -761,9 +800,9 @@ initializeKernel outputChannel = do
       bind b val
       addToKernel name runtime b
 
-    addUniversalPrimitive :: Text -> (MacroDest -> Syntax -> Expand ()) -> Expand ()
-    addUniversalPrimitive name impl = do
-      let val = EPrimUniversalMacro impl
+    addPolyProblemPrimitive :: Text -> (MacroDest -> Syntax -> Expand ()) -> Expand ()
+    addPolyProblemPrimitive name impl = do
+      let val = EPrimPolyProblemMacro impl
       b <- freshBinding
       bind b val
       addToKernel name runtime b
@@ -895,6 +934,8 @@ runTask (tid, localData, task) = withLocal localData $ do
           expandOnePattern scrutT d stx
         TypePatternDest d ->
           expandOneTypePattern d stx
+        TypeCtorDest d ->
+          expandOneTypeCtor d stx
     AwaitingType tdest after ->
       linkedType tdest >>=
       \case
@@ -915,6 +956,7 @@ runTask (tid, localData, task) = withLocal localData $ do
             Ty (TyF (TMetaVar ptr) _) | ptr == ptr' -> stillStuck tid task
             _ -> forkAwaitingTypeCase loc dest (tMetaVar ptr') env cases kont
         other -> do
+          -- TODO: should this expandEval be 'inEarlierPhase'?
           selectedBranch <- expandEval $ withEnv env $ doTypeCase loc (Ty other) cases
           case selectedBranch of
             ValueMacroAction nextStep -> do
@@ -974,7 +1016,7 @@ runTask (tid, localData, task) = withLocal localData $ do
         Just newScopeSet ->
           expandDeclForms dest (earlierScopeSet <> newScopeSet) outScopesDest (addScopes newScopeSet stx)
     InterpretMacroAction dest act outerKont ->
-      interpretMacroAction dest act >>= \case
+      inEarlierPhase (interpretMacroAction dest act) >>= \case
         StuckOnType loc ty env cases innerKont ->
           forkAwaitingTypeCase loc dest ty env cases (innerKont ++ outerKont)
         Done value -> do
@@ -985,11 +1027,11 @@ runTask (tid, localData, task) = withLocal localData $ do
           forkExpandSyntax dest syntax
         other -> expandEval $ evalErrorType "syntax" other
     ContinueMacroAction dest value (closure:kont) -> do
-      result <- expandEval $ apply closure value
+      result <- inEarlierPhase $ expandEval $ apply closure value
       case result of
         ValueMacroAction macroAction -> do
           forkInterpretMacroAction dest macroAction kont
-        other -> expandEval $ evalErrorType "macro action" other
+        other -> inEarlierPhase $ expandEval $ evalErrorType "macro action" other
     EvalDefnAction x n p expr ->
       linkedCore expr >>=
       \case
@@ -1131,6 +1173,10 @@ expandOneTypePattern :: TypePatternPtr -> Syntax -> Expand ()
 expandOneTypePattern dest stx =
   expandOneForm (TypePatternDest dest) stx
 
+expandOneTypeCtor :: TypeCtorPtr -> Syntax -> Expand ()
+expandOneTypeCtor dest stx =
+  expandOneForm (TypeCtorDest dest) stx
+
 
 
 -- | Insert a function application marker with a lexical context from
@@ -1159,40 +1205,44 @@ addStringLiteral (Syntax (Stx scs loc _)) s =
     stringLiteral = Syntax (Stx scs loc (Id "#%string-literal"))
     s' = Syntax (Stx scs loc (String s))
 
-problemCategory :: MacroDest -> SyntacticCategory
-problemCategory (ModuleDest {}) = ModuleCat
-problemCategory (DeclTreeDest {}) = DeclarationCat
-problemCategory (TypeDest {}) = TypeCat
-problemCategory (ExprDest {}) = ExpressionCat
-problemCategory (PatternDest {}) = PatternCaseCat
-problemCategory (TypePatternDest {}) = TypePatternCaseCat
-
 requireDeclarationCat :: Syntax -> MacroDest -> Expand (DeclTreePtr, DeclOutputScopesPtr)
 requireDeclarationCat _ (DeclTreeDest dest outScopesDest) = return (dest, outScopesDest)
 requireDeclarationCat stx other =
   throwError $
-  WrongSyntacticCategory stx (tenon DeclarationCat) (mortise $ problemCategory other)
+  WrongSyntacticCategory stx (tenon DeclarationCat :| []) (mortise $ problemCategory other)
 
 requireTypeCat :: Syntax -> MacroDest -> Expand (Kind, SplitTypePtr)
 requireTypeCat _ (TypeDest kind dest) = return (kind, dest)
 requireTypeCat stx other =
   throwError $
-  WrongSyntacticCategory stx (tenon TypeCat) (mortise $ problemCategory other)
+  WrongSyntacticCategory stx (tenon TypeCat :| []) (mortise $ problemCategory other)
 
 requireExpressionCat :: Syntax -> MacroDest -> Expand (Ty, SplitCorePtr)
 requireExpressionCat _ (ExprDest ty dest) = return (ty, dest)
 requireExpressionCat stx other =
   throwError $
-  WrongSyntacticCategory stx (tenon ExpressionCat) (mortise $ problemCategory other)
+  WrongSyntacticCategory stx (tenon ExpressionCat :| []) (mortise $ problemCategory other)
 
-requirePatternCat :: Syntax -> MacroDest -> Expand (Either (Ty, PatternPtr) TypePatternPtr)
+requirePatternCat :: Syntax -> MacroDest -> Expand (Ty, PatternPtr)
 requirePatternCat _ (PatternDest scrutTy dest) =
-  return $ Left (scrutTy, dest)
-requirePatternCat _ (TypePatternDest dest) =
-  return $ Right dest
+  return (scrutTy, dest)
 requirePatternCat stx other =
   throwError $
-  WrongSyntacticCategory stx (tenon PatternCaseCat) (mortise $ problemCategory other)
+  WrongSyntacticCategory stx (tenon PatternCat :| []) (mortise $ problemCategory other)
+
+requireTypePatternCat :: Syntax -> MacroDest -> Expand TypePatternPtr
+requireTypePatternCat _ (TypePatternDest dest) =
+  return dest
+requireTypePatternCat stx other =
+  throwError $
+  WrongSyntacticCategory stx (tenon TypePatternCat :| []) (mortise $ problemCategory other)
+
+requireTypeCtorCat :: Syntax -> MacroDest -> Expand TypeCtorPtr
+requireTypeCtorCat _ (TypeCtorDest dest) =
+  return dest
+requireTypeCtorCat stx other =
+  throwError $
+  WrongSyntacticCategory stx (tenon TypeCtorCat :| []) (mortise $ problemCategory other)
 
 
 expandOneForm :: MacroDest -> Syntax -> Expand ()
@@ -1238,17 +1288,17 @@ expandOneForm prob stx
                     pure ptr
                   modifyState $ set (expanderPatternBinders . at dest) $ Just $ Left subPtrs
                   linkPattern dest $
-                    CtorPattern ctor subPtrs
+                    DataCtorPattern ctor subPtrs
             other ->
               throwError $
-              WrongSyntacticCategory stx (tenon ExpressionCat) (mortise $ problemCategory other)
+              WrongSyntacticCategory stx (tenon ExpressionCat :| []) (mortise $ problemCategory other)
         EPrimModuleMacro impl ->
           case prob of
             ModuleDest dest -> do
               impl dest stx
             other ->
               throwError $
-              WrongSyntacticCategory stx (tenon ModuleCat) (mortise $ problemCategory other)
+              WrongSyntacticCategory stx (tenon ModuleCat :| []) (mortise $ problemCategory other)
         EPrimDeclMacro impl -> do
           (dest, outScopesDest) <- requireDeclarationCat stx prob
           impl dest outScopesDest stx
@@ -1260,11 +1310,17 @@ expandOneForm prob stx
               implP dest stx
             otherDest ->
               throwError $
-              WrongSyntacticCategory stx (tenon TypeCat) (mortise $ problemCategory otherDest)
+              WrongSyntacticCategory stx (tenon TypeCat :| []) (mortise $ problemCategory otherDest)
         EPrimPatternMacro impl -> do
-          dest <- requirePatternCat stx prob
+          (scrutTy, dest) <- requirePatternCat stx prob
+          impl scrutTy dest stx
+        EPrimTypePatternMacro impl -> do
+          dest <- requireTypePatternCat stx prob
+          impl dest stx
+        EPrimTypeCtorMacro impl -> do
+          dest <- requireTypeCtorCat stx prob
           impl dest stx
-        EPrimUniversalMacro impl ->
+        EPrimPolyProblemMacro impl ->
           impl prob stx
         EVarMacro var -> do
           (t, dest) <- requireExpressionCat stx prob
@@ -1306,7 +1362,7 @@ expandOneForm prob stx
                           ValueSyntax $ addScope p stepScope stx
               case macroVal of
                 ValueMacroAction act -> do
-                  res <- interpretMacroAction prob act
+                  res <- inEarlierPhase $ interpretMacroAction prob act
                   case res of
                     StuckOnType loc ty env cases kont ->
                       forkAwaitingTypeCase loc prob ty env cases kont
@@ -1340,6 +1396,8 @@ expandOneForm prob stx
         throwError $ InternalError "All patterns should be identifier-headed"
       TypePatternDest {} ->
         throwError $ InternalError "All type patterns should be identifier-headed"
+      TypeCtorDest {} ->
+        throwError $ InternalError "All type constructors should be identifier-headed"
 
 
 expandModuleForm :: DeclTreePtr -> Syntax -> Expand ()
@@ -1432,8 +1490,8 @@ interpretMacroAction prob =
         getIdent (ValueSyntax stx) = mustBeIdent stx
         getIdent _other = throwError $ InternalError $ "Not a syntax object in " ++ opName
         compareFree id1 id2 = do
-          b1 <- resolve id1
-          b2 <- resolve id2
+          b1 <- inLaterPhase $ resolve id1
+          b2 <- inLaterPhase $ resolve id2
           return $ Done $
             flip primitiveCtor [] $
             if b1 == b2 then "true" else "false"
@@ -1462,5 +1520,6 @@ interpretMacroAction prob =
         ExprDest t _stx -> pure $ Done $ primitiveCtor "expression" [ValueType t]
         PatternDest {} -> pure $ Done $ primitiveCtor "pattern" []
         TypePatternDest {} -> pure $ Done $ primitiveCtor "type-pattern" []
+        TypeCtorDest {} -> pure $ Done $ primitiveCtor "type-constructor" []
     MacroActionTypeCase env loc ty cases -> do
       pure $ StuckOnType loc ty env cases []
diff --git a/src/Expander/Error.hs b/src/Expander/Error.hs
index c4134733..a31acd96 100644
--- a/src/Expander/Error.hs
+++ b/src/Expander/Error.hs
@@ -1,10 +1,12 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE DerivingStrategies    #-}
+{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE OverloadedStrings     #-}
+{-# LANGUAGE UndecidableInstances #-}
 module Expander.Error
   ( ExpansionErr(..)
-  , SyntacticCategory(..)
+  , SyntacticCategory(..), problemCategory
   , TypeCheckError(..)
   , Tenon, tenon, Mortise, mortise
   , notRightLength
@@ -12,6 +14,7 @@ module Expander.Error
 
 import Control.Lens
 import Numeric.Natural
+import Data.List.NonEmpty (NonEmpty((:|)))
 import Data.Text (Text)
 import Data.Sequence (Seq)
 import qualified Data.Text as T
@@ -44,7 +47,7 @@ data ExpansionErr
   | NotInteger Syntax
   | NotString Syntax
   | NotModName Syntax
-  | NotRightLength [Natural] Syntax
+  | NotRightLength (NonEmpty Natural) Syntax
   | NotVec Syntax
   | NotImportSpec Syntax
   | NotExportSpec Syntax
@@ -59,7 +62,7 @@ data ExpansionErr
   | NotExported Ident Phase
   | ReaderError Text
   | WrongSyntacticCategory Syntax
-      (Tenon SyntacticCategory)
+      (NonEmpty (Tenon SyntacticCategory))
       (Mortise SyntacticCategory)
   | NotValidType Syntax
   | TypeCheckError TypeCheckError
@@ -89,7 +92,7 @@ tenon :: a -> Tenon a
 tenon = Tenon
 
 notRightLength :: Natural -> Syntax -> ExpansionErr
-notRightLength n = NotRightLength [n]
+notRightLength n = NotRightLength (n :| [])
 
 data TypeCheckError
   = TypeMismatch (Maybe SrcLoc) Ty Ty (Maybe (Ty, Ty))
@@ -103,10 +106,31 @@ data SyntacticCategory
   | DeclarationCat
   | TypeCat
   | ExpressionCat
-  | PatternCaseCat
-  | TypePatternCaseCat
+  | PatternCat
+  | TypePatternCat
+  | TypeCtorCat
   deriving Show
 
+problemCategory :: MacroDest -> SyntacticCategory
+problemCategory (ModuleDest {}) = ModuleCat
+problemCategory (DeclTreeDest {}) = DeclarationCat
+problemCategory (TypeDest {}) = TypeCat
+problemCategory (ExprDest {}) = ExpressionCat
+problemCategory (PatternDest {}) = PatternCat
+problemCategory (TypePatternDest {}) = TypePatternCat
+problemCategory (TypeCtorDest {}) = TypeCtorCat
+
+alts
+  :: NonEmpty (Doc ann) -> Doc ann
+alts (x :| [])
+  = x
+alts (x :| y : [])
+  = x <> " or " <> y
+alts (x :| y : z : [])
+  = x <> ", " <> y <> ", or " <> z
+alts (x1 :| x2 : xs)
+  = x1 <> ", " <> alts (x2 :| xs)
+
 instance Pretty VarInfo ExpansionErr where
   pp env (Ambiguous p x candidates) =
     hang 4 $
@@ -148,19 +172,9 @@ instance Pretty VarInfo ExpansionErr where
          ]
   pp env (NotRightLength lengths0 stx) =
     hang 2 $ group $
-    vsep [ text "Expected" <+> alts lengths0 <+> text "entries between parentheses, but got"
+    vsep [ text "Expected" <+> alts (fmap viaShow lengths0) <+> text "entries between parentheses, but got"
          , pp env stx
          ]
-    where
-      alts :: [Natural] -> Doc ann
-      alts []
-        = error "internal error: NotRightLength doesn't offer any acceptable lengths"
-      alts [len]
-        = viaShow len
-      alts [len1, len2]
-        = viaShow len1 <+> "or" <+> viaShow len2
-      alts (len:lengths)
-        = viaShow len <> "," <+> alts lengths
   pp env (NotVec stx) =
     hang 2 $ group $ vsep [text "Expected square-bracketed vec but got", pp env stx]
   pp env (NotImportSpec stx) =
@@ -200,16 +214,16 @@ instance Pretty VarInfo ExpansionErr where
     text "Internal error during expansion! This is a bug in the implementation." <> line <> string str
   pp _env (ReaderError txt) =
     vsep (map text (T.lines txt))
-  pp env (WrongSyntacticCategory stx is shouldBe) =
+  pp env (WrongSyntacticCategory stx tenons _mortise) =
     hang 2 $ group $
     vsep [ pp env stx <> text ":"
          , group $ vsep [ group $ hang 2 $
                           vsep [ text "Used in a position expecting"
-                               , pp env (unMortise shouldBe)
+                               , pp env $ unMortise _mortise
                                ]
                         , group $ hang 2 $
                           vsep [ text "but is valid in a position expecting"
-                               , pp env (unTenon is)
+                               , alts $ fmap (pp env . unTenon) tenons
                                ]
                         ]
          ]
@@ -275,5 +289,6 @@ instance Pretty VarInfo SyntacticCategory where
   pp _env ModuleCat = text "a module"
   pp _env TypeCat = text "a type"
   pp _env DeclarationCat = text "a top-level declaration or example"
-  pp _env PatternCaseCat = text "a pattern"
-  pp _env TypePatternCaseCat = text "a typecase pattern"
+  pp _env PatternCat = text "a pattern"
+  pp _env TypePatternCat = text "a typecase pattern"
+  pp _env TypeCtorCat = text "a type constructor"
diff --git a/src/Expander/Monad.hs b/src/Expander/Monad.hs
index 7a8c34c4..3a56599f 100644
--- a/src/Expander/Monad.hs
+++ b/src/Expander/Monad.hs
@@ -45,6 +45,7 @@ module Expander.Monad
   , getDecl
   , getState
   , inEarlierPhase
+  , inLaterPhase
   , inPhase
   , isExprChecked
   , importing
@@ -187,7 +188,6 @@ import KlisterPath
 import PartialCore
 import PartialType
 import Phase
-import ShortShow
 import SplitCore
 import SplitType
 import Scope
@@ -237,8 +237,10 @@ data EValue
     -- ^ For type-level special forms - first as types, then as type patterns
   | EPrimModuleMacro (DeclTreePtr -> Syntax -> Expand ())
   | EPrimDeclMacro (DeclTreePtr -> DeclOutputScopesPtr -> Syntax -> Expand ())
-  | EPrimPatternMacro (Either (Ty, PatternPtr) TypePatternPtr -> Syntax -> Expand ())
-  | EPrimUniversalMacro (MacroDest -> Syntax -> Expand ())
+  | EPrimPatternMacro (Ty -> PatternPtr -> Syntax -> Expand ())
+  | EPrimTypePatternMacro (TypePatternPtr -> Syntax -> Expand ())
+  | EPrimTypeCtorMacro (TypeCtorPtr -> Syntax -> Expand ())
+  | EPrimPolyProblemMacro (MacroDest -> Syntax -> Expand ())
   | EVarMacro !Var -- ^ For bound variables (the Unique is the binding site of the var)
   | ETypeVar !Kind !Natural
   -- ^ For bound type variables (user-written Skolem variables or in datatype definitions)
@@ -286,7 +288,7 @@ data ExpanderState = ExpanderState
   , _expanderTasks              :: [(TaskID, ExpanderLocal, ExpanderTask)]
   , _expanderOriginLocations    :: !(Store SplitCorePtr SrcLoc)
   , _expanderCompletedCore      :: !(Store SplitCorePtr (CoreF TypePatternPtr PatternPtr SplitCorePtr))
-  , _expanderCompletedPatterns  :: !(Store PatternPtr (ConstructorPatternF PatternPtr))
+  , _expanderCompletedPatterns  :: !(Store PatternPtr (DataPatternF PatternPtr))
   , _expanderCompletedTypePatterns :: !(Store TypePatternPtr TypePattern)
   , _expanderPatternBinders     :: !(Store PatternPtr (Either [PatternPtr] (Scope, Ident, Var, SchemePtr)))
   , _expanderTypePatternBinders :: !(Store TypePatternPtr [(Scope, Ident, Var, SchemePtr)])
@@ -407,6 +409,10 @@ inEarlierPhase :: Expand a -> Expand a
 inEarlierPhase act =
   Expand $ local (over (expanderLocal . expanderPhase) prior) $ runExpand act
 
+inLaterPhase :: Expand a -> Expand a
+inLaterPhase act =
+  Expand $ local (over (expanderLocal . expanderPhase) posterior) $ runExpand act
+
 moduleScope :: ModuleName -> Expand Scope
 moduleScope mn = moduleScope' mn
 
@@ -442,7 +448,7 @@ linkExpr :: SplitCorePtr -> CoreF TypePatternPtr PatternPtr SplitCorePtr -> Expa
 linkExpr dest layer =
   modifyState $ over expanderCompletedCore (<> S.singleton dest layer)
 
-linkPattern :: PatternPtr -> ConstructorPatternF PatternPtr -> Expand ()
+linkPattern :: PatternPtr -> DataPatternF PatternPtr -> Expand ()
 linkPattern dest pat =
   modifyState $ over expanderCompletedPatterns (<> S.singleton dest pat)
 
diff --git a/src/Expander/Primitives.hs b/src/Expander/Primitives.hs
index b8c5b8f8..1f1d0cb7 100644
--- a/src/Expander/Primitives.hs
+++ b/src/Expander/Primitives.hs
@@ -6,9 +6,11 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE ViewPatterns #-}
 {-# OPTIONS -Wno-name-shadowing #-}
+{-# OPTIONS -Wno-incomplete-uni-patterns #-}
 module Expander.Primitives
   ( -- * Declaration primitives
-    define
+    DeclPrim
+  , define
   , datatype
   , defineMacros
   , example
@@ -16,6 +18,7 @@ module Expander.Primitives
   , group
   , meta
   -- * Expression primitives
+  , ExprPrim
   , app
   , integerLiteral
   , stringLiteral
@@ -44,11 +47,18 @@ module Expander.Primitives
   , the
   , typeCase
   -- * Pattern primitives
-  , elsePattern
+  , PatternPrim
+  -- * Type pattern primitives
+  , TypePatternPrim
+  -- * Type constructor primitives
+  , TypeCtorPrim
   -- * Module primitives
+  , ModulePrim
   , makeModule
-  -- * Anywhere primitives
+  -- * Poly-Problem primitives
+  , PolyProblemPrim
   , makeLocalType
+  , elsePattern
   -- * Primitive values
   , unaryIntegerPrim
   , binaryIntegerPrim
@@ -65,6 +75,7 @@ import Control.Lens hiding (List)
 import Control.Monad.IO.Class
 import Control.Monad
 import Control.Monad.Except
+import Data.List.NonEmpty (NonEmpty((:|)))
 import Data.Text (Text)
 import qualified Data.Text as T
 import Data.Traversable
@@ -85,7 +96,6 @@ import Phase
 import Scope
 import ScopeSet (ScopeSet)
 import qualified ScopeSet
-import ShortShow
 import SplitCore
 import SplitType
 import Syntax
@@ -538,9 +548,9 @@ typeConstructor ctor argKinds = (implT, implP)
           sch <- trivialScheme tType
           -- FIXME kind check here
           linkTypePattern dest
-            (TypePattern $ TyF ctor [ (varStx, var)
-                                    | (_, varStx, var) <- varInfo
-                                    ])
+            (TypeCtorPattern $ TyF ctor [ (varStx, var)
+                                        | (_, varStx, var) <- varInfo
+                                        ])
             [ (sc, n, x, sch)
             | (sc, n, x) <- varInfo
             ]
@@ -552,7 +562,9 @@ baseType ctor = typeConstructor ctor []
 -- Modules --
 -------------
 
-makeModule :: DeclExpander -> DeclTreePtr -> Syntax -> Expand ()
+type ModulePrim = DeclTreePtr -> Syntax -> Expand ()
+
+makeModule :: DeclExpander -> ModulePrim
 makeModule expandDeclForms bodyPtr stx =
   view expanderModuleTop <$> getState >>=
   \case
@@ -568,13 +580,79 @@ makeModule expandDeclForms bodyPtr stx =
       pure ()
 
 --------------
--- Anywhere --
+-- Patterns --
 --------------
 
--- | with-unknown-type's implementation: create a named fresh
--- unification variable for macros that only can annotate part of a
--- type.
-makeLocalType :: MacroDest -> Syntax -> Expand ()
+type PatternPrim = Ty -> PatternPtr -> Syntax -> Expand ()
+
+-------------------
+-- Type Patterns --
+-------------------
+
+type TypePatternPrim = TypePatternPtr -> Syntax -> Expand ()
+
+-----------------------
+-- Type Constructors --
+-----------------------
+
+type TypeCtorPrim = TypeCtorPtr -> Syntax -> Expand ()
+
+------------------
+-- Poly-Problem --
+------------------
+
+type PolyProblemPrim = MacroDest -> Syntax -> Expand ()
+
+-- | with-unknown-type binds a fresh unification variable.
+--
+-- with-unknown-type works in any Problem. In a type, it acts like a named
+-- wildcard in Haskell. That is,
+--
+-- > (example
+-- >   (the (with-unknown-type [_i]
+-- >          (-> (Pair Integer _i)
+-- >              (Pair _i Integer)))
+-- >        id))
+--
+-- infers to
+--
+-- > (example
+-- >   (the (-> (Pair Integer Integer)
+-- >            (Pair Integer Integer))
+-- >        id))
+--
+-- In an expression, with-unknown-type makes it possible to specify that
+-- multiple parts of that expression must have related types. For example,
+--
+-- > (example
+-- >   (with-unknown-type [_i2i]
+-- >      (pair (the _i2i negate)
+-- >            (the _i2i id))))
+--
+-- infers to
+--
+-- > (example
+-- >   (pair (the (-> Integer Integer) negate)
+-- >         (the (-> Integer Integer) id)))
+--
+-- And in a declaration block, with-unknown-type makes it possible to specify
+-- that multiple declarations must have related types. For example,
+--
+-- > (with-unknown-type [_i2i]
+-- >   (group
+-- >     (example (the _i2i negate))
+-- >     (example (the _i2i id))))
+--
+-- infers to
+--
+-- > (group
+-- >   (example (the (-> Integer Integer) negate))
+-- >   (example (the (-> Integer Integer) id)))
+--
+-- If there were pattern macros which took a type as an argument,
+-- with-unknown-type would be useful in those Problems as well, to bind a
+-- unification variable whose scope is limited to a portion of that pattern.
+makeLocalType :: PolyProblemPrim
 makeLocalType dest stx = do
   Stx _ _ (_, binder, body) <- mustHaveEntries stx
   Stx _ _ (Identity theVar) <- mustHaveEntries binder
@@ -596,27 +674,26 @@ makeLocalType dest stx = do
 
   forkExpandSyntax dest (addScope p sc body)
 
---------------
--- Patterns --
---------------
-
-type PatternPrim = Either (Ty, PatternPtr) TypePatternPtr -> Syntax -> Expand ()
-
-elsePattern :: PatternPrim
-elsePattern (Left (scrutTy, dest)) stx = do
+elsePattern :: PolyProblemPrim
+elsePattern (PatternDest scrutTy dest) stx = do
   Stx _ _ (_, var) <- mustHaveEntries stx
   ty <- trivialScheme scrutTy
   (sc, x, v) <- prepareVar var
   modifyState $ set (expanderPatternBinders . at dest) $
     Just $ Right (sc, x, v, ty)
   linkPattern dest $ PatternVar x v
-elsePattern (Right dest) stx = do
+elsePattern (TypePatternDest dest) stx = do
   Stx _ _ (_, var) <- mustHaveEntries stx
   ty <- trivialScheme tType
   (sc, x, v) <- prepareVar var
   linkTypePattern dest
-    (AnyType x v)
+    (TypePatternVar x v)
     [(sc, x, v, ty)]
+elsePattern other stx = do
+  throwError $
+    WrongSyntacticCategory stx
+      (tenon PatternCat :| tenon TypePatternCat : [])
+      (mortise $ problemCategory other)
 
 -------------
 -- Helpers --
diff --git a/src/Expander/Syntax.hs b/src/Expander/Syntax.hs
index 2a3202b5..9da735bd 100644
--- a/src/Expander/Syntax.hs
+++ b/src/Expander/Syntax.hs
@@ -10,7 +10,8 @@ module Expander.Syntax where
 import Control.Monad.Except
 import Control.Monad.IO.Class
 import Data.Functor.Identity (Identity(Identity))
-import Data.List (nub, sort)
+import Data.List.NonEmpty (NonEmpty((:|)))
+import qualified Data.List.NonEmpty as NonEmpty
 import Data.Text (Text)
 import qualified Data.Text as T
 import Numeric.Natural
@@ -79,7 +80,7 @@ mustHaveEntries other = do
   throwError (NotList other)
 
 class FixedLengthList item r where
-  checkLength :: [item] -> Either [Natural] r
+  checkLength :: [item] -> Either (NonEmpty Natural) r
 
 instance ( FixedLengthList item a
          , FixedLengthList item b
@@ -92,43 +93,43 @@ instance ( FixedLengthList item a
         (_, Right b)
           -> pure (Right b)
         (Left lengths1, Left lengths2)
-          -> Left $ nub $ sort (lengths1 ++ lengths2)
+          -> Left $ NonEmpty.nub $ NonEmpty.sort (lengths1 <> lengths2)
 
 instance FixedLengthList item () where
   checkLength []
     = pure ()
   checkLength _
-    = Left [0]
+    = Left (0 :| [])
 
 instance a ~ item => FixedLengthList item (Identity a) where
   checkLength [x]
     = pure (Identity x)
   checkLength _
-    = Left [1]
+    = Left (1 :| [])
 
 instance (a ~ item, b ~ item) => FixedLengthList item (a, b) where
   checkLength [x, y]
     = return (x, y)
   checkLength _
-    = Left [2]
+    = Left (2 :| [])
 
 instance (a ~ item, b ~ item, c ~ item) => FixedLengthList item (a, b, c) where
   checkLength [x, y, z]
     = pure (x, y, z)
   checkLength _
-    = Left [3]
+    = Left (3 :| [])
 
 instance (a ~ item, b ~ item, c ~ item, d ~ item) => FixedLengthList item (a, b, c, d) where
   checkLength [w, x, y, z]
     = pure (w, x, y, z)
   checkLength _
-    = Left [4]
+    = Left (4 :| [])
 
 instance (a ~ item, b ~ item, c ~ item, d ~ item, e ~ item) => FixedLengthList item (a, b, c, d, e) where
   checkLength [v, w, x, y, z]
     = pure (v, w, x, y, z)
   checkLength _
-    = Left [5]
+    = Left (5 :| [])
 
 
 class MustHaveShape a where
diff --git a/src/Expander/Task.hs b/src/Expander/Task.hs
index d4a3707b..eb60183e 100644
--- a/src/Expander/Task.hs
+++ b/src/Expander/Task.hs
@@ -2,8 +2,6 @@
 {-# LANGUAGE OverloadedStrings #-}
 module Expander.Task where
 
-import qualified Data.Text as T
-
 import Binding
 import Core
 import Datatype
@@ -11,9 +9,7 @@ import Expander.DeclScope
 import Kind
 import Module
 import Phase
-import Pretty
 import ScopeSet
-import ShortShow
 import SplitCore
 import SplitType
 import Syntax
@@ -33,6 +29,8 @@ data MacroDest
     -- ^ scrutinee type, destination pointer
   | TypePatternDest TypePatternPtr
     -- ^ destination pointer
+  | TypeCtorDest TypeCtorPtr
+    -- ^ destination pointer
   deriving Show
 
 
@@ -83,31 +81,3 @@ data TaskAwaitMacroType = TaskAwaitMacroType
   , awaitMacroTypeSyntax :: Syntax -- the syntax object to be expanded once the macro is available
   }
   deriving (Show)
-
-
-instance ShortShow TaskAwaitMacro where
-  shortShow (TaskAwaitMacro _ _ x deps _ stx) =
-    "(TaskAwaitMacro " ++ show x ++ " " ++ show deps ++ " " ++ T.unpack (pretty stx) ++ ")"
-
-instance ShortShow TaskAwaitMacroType where
-  shortShow = show
-
-instance ShortShow ExpanderTask where
-  shortShow (ExpandSyntax _dest stx) = "(ExpandSyntax " ++ T.unpack (pretty stx) ++ ")"
-  shortShow (AwaitingTypeCase loc _ _ _ _ _) = "(AwaitingTypeCase " ++ shortShow loc ++ "_)"
-  shortShow (AwaitingDefn _x n _b _defn _t _dest stx) =
-    "(AwaitingDefn " ++ shortShow n ++ " " ++ shortShow stx ++ ")"
-  shortShow (AwaitingMacro dest t) = "(AwaitingMacro " ++ show dest ++ " " ++ shortShow t ++ ")"
-  shortShow (AwaitingType tdest tasks) = "(AwaitingType " ++ show tdest ++ " " ++ show tasks ++ ")"
-  shortShow (ExpandDeclForms _dest _scs waitingOn outScopesDest stx) = "(ExpandDeclForms _ " ++ show waitingOn ++ " " ++ show outScopesDest ++ " " ++ T.unpack (syntaxText stx) ++ ")"
-  shortShow (InterpretMacroAction _dest act kont) = "(InterpretMacroAction " ++ show act ++ " " ++ show kont ++ ")"
-  shortShow (ContinueMacroAction _dest value kont) = "(ContinueMacroAction " ++ show value ++ " " ++ show kont ++ ")"
-  shortShow (EvalDefnAction var name phase _expr) = "(EvalDefnAction " ++ show var ++ " " ++ shortShow name ++ " " ++ show phase ++ ")"
-  shortShow (GeneralizeType e _ _) = "(GeneralizeType " ++ show e ++ " _ _)"
-  shortShow (ExpandVar t d x v) = "(ExpandVar " ++ show t ++ " " ++ show d ++ " " ++ show x ++ " " ++ show v ++ ")"
-  shortShow (EstablishConstructors _ _ dt _) = "(EstablishConstructors " ++ show dt ++ ")"
-  shortShow (AwaitingPattern _ _ _ _) = "(AwaitingPattern _ _ _ _)"
-  shortShow (AwaitingTypePattern _ _ _ _) = "(AwaitingTypePattern _ _ _ _)"
-
-instance Pretty VarInfo ExpanderTask where
-  pp _ task = string (shortShow task)
diff --git a/src/ModuleName.hs b/src/ModuleName.hs
index 16bbc9a4..6eb409f1 100644
--- a/src/ModuleName.hs
+++ b/src/ModuleName.hs
@@ -20,8 +20,6 @@ import System.FilePath
 import Data.Hashable
 import GHC.Generics (Generic)
 
-import ShortShow
-
 newtype KernelName = Kernel ()
   deriving (Data, Eq, Ord, Show, Generic)
 
@@ -35,10 +33,6 @@ data ModuleName = ModuleName FilePath | KernelName KernelName
 
 instance Hashable ModuleName
 
-instance ShortShow ModuleName where
-  shortShow (ModuleName x) = x
-  shortShow (KernelName _k) = "kernel"
-
 moduleNameFromPath :: FilePath -> IO ModuleName
 moduleNameFromPath file = ModuleName <$> canonicalizePath file
 
diff --git a/src/PartialCore.hs b/src/PartialCore.hs
index 4ae9a695..a84002b6 100644
--- a/src/PartialCore.hs
+++ b/src/PartialCore.hs
@@ -6,7 +6,7 @@ import Control.Lens
 import Core
 
 newtype PartialPattern =
-  PartialPattern { unPartialPattern :: Maybe (ConstructorPatternF PartialPattern) }
+  PartialPattern { unPartialPattern :: Maybe (DataPatternF PartialPattern) }
   deriving (Eq, Show)
 
 newtype PartialCore = PartialCore
@@ -20,12 +20,12 @@ nonPartial :: Core -> PartialCore
 nonPartial =
   PartialCore . Just . mapCoreF Just nonPartialPattern nonPartial . unCore
   where
-    nonPartialPattern pat = PartialPattern $ Just $ nonPartialPattern <$> unConstructorPattern pat
+    nonPartialPattern pat = PartialPattern $ Just $ nonPartialPattern <$> unDataPattern pat
 
 runPartialCore :: PartialCore -> Maybe Core
 runPartialCore (PartialCore Nothing) = Nothing
 runPartialCore (PartialCore (Just c)) = Core <$> traverseCoreF id runPartialPattern runPartialCore c
 
-runPartialPattern :: PartialPattern -> Maybe ConstructorPattern
+runPartialPattern :: PartialPattern -> Maybe DataPattern
 runPartialPattern (PartialPattern Nothing) = Nothing
-runPartialPattern (PartialPattern (Just p)) = ConstructorPattern <$> traverse runPartialPattern p
+runPartialPattern (PartialPattern (Just p)) = DataPattern <$> traverse runPartialPattern p
diff --git a/src/Phase.hs b/src/Phase.hs
index b622e0a7..abe038b4 100644
--- a/src/Phase.hs
+++ b/src/Phase.hs
@@ -3,15 +3,13 @@
 {-# LANGUAGE TemplateHaskell    #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 
-module Phase (Phase(..), runtime, prior, Phased(..)) where
+module Phase (Phase(..), runtime, prior, posterior, Phased(..)) where
 
 import Control.Lens
 import Data.Data (Data)
 import Data.Sequence (Seq)
 import Numeric.Natural
 
-import ShortShow
-
 import Util.Key
 
 newtype Phase = Phase { phaseNum :: Natural }
@@ -25,15 +23,15 @@ instance HasKey Phase where
   {-# INLINE getKey  #-}
   {-# INLINE fromKey #-}
 
-instance ShortShow Phase where
-  shortShow (Phase i) = "p" ++ show i
-
 runtime :: Phase
 runtime = Phase 0
 
 prior :: Phase -> Phase
 prior (Phase i) = Phase (i + 1)
 
+posterior :: Phase -> Phase
+posterior (Phase i) = Phase (i - 1)
+
 class Phased a where
   shift :: Natural -> a -> a
 
diff --git a/src/Pretty.hs b/src/Pretty.hs
index 238d37c5..547e0a3e 100644
--- a/src/Pretty.hs
+++ b/src/Pretty.hs
@@ -26,6 +26,7 @@ import Binding.Info
 import Core
 import Datatype
 import Env
+import Expander.Task
 import Evaluator (EvalResult(..), EvalError(..), TypeError(..))
 import Kind
 import Module
@@ -34,6 +35,7 @@ import KlisterPath
 import Phase
 import Scope
 import ScopeSet
+import SplitCore
 import Syntax
 import Syntax.SrcLoc
 import Type
@@ -210,16 +212,16 @@ instance PrettyBinder VarInfo BinderPair where
     (annotate (BindingSite x) (text n), Env.singleton x ident ())
 
 instance PrettyBinder VarInfo TypePattern where
-  ppBind env (TypePattern t) =
+  ppBind env (TypeCtorPattern t) =
     ppBind env (fmap BinderPair t)
-  ppBind env (AnyType ident x) =
+  ppBind env (TypePatternVar ident x) =
     ppBind env (BinderPair (ident, x))
 
-instance PrettyBinder VarInfo ConstructorPattern where
-  ppBind env pat = ppBind env (unConstructorPattern pat)
+instance PrettyBinder VarInfo DataPattern where
+  ppBind env pat = ppBind env (unDataPattern pat)
 
-instance PrettyBinder VarInfo a => PrettyBinder VarInfo (ConstructorPatternF a) where
-  ppBind env (CtorPattern ctor subPats) =
+instance PrettyBinder VarInfo a => PrettyBinder VarInfo (DataPatternF a) where
+  ppBind env (DataCtorPattern ctor subPats) =
     case subPats of
       [] -> (pp env ctor, Env.empty)
       _nonEmpty ->
@@ -674,3 +676,71 @@ instance Pretty VarInfo ScopeSet where
 
 instance Pretty VarInfo KlisterPathError where
   pp _ = ppKlisterPathError
+
+
+instance Pretty VarInfo TaskAwaitMacro where
+  pp env (TaskAwaitMacro _ _ x deps _ stx) =
+    "(TaskAwaitMacro" <+>
+    pp env x <+>
+    vec (hsep $ map (pp env) deps) <+>
+    pp env stx <>
+    ")"
+
+instance Pretty VarInfo TaskAwaitMacroType where
+  pp env (TaskAwaitMacroType _ _ x _ stx) =
+    "(TaskAwaitMacroType" <+> pp env x <+> pp env stx <> ")"
+
+instance Pretty VarInfo ExpanderTask where
+  pp env (ExpandSyntax _dest stx) =
+    "(ExpandSyntax" <+> pp env stx <> ")"
+  pp env (AwaitingTypeCase loc _ _ _ _ _) =
+    "(AwaitingTypeCase" <+> pp env loc <+> "_)"
+  pp env (AwaitingDefn _x n _b _defn _t _dest stx) =
+    "(AwaitingDefn" <+> pp env n <+> pp env stx <> ")"
+  pp env (AwaitingMacro dest t) =
+    "(AwaitingMacro" <+> pp env dest <+> pp env t <> ")"
+  pp env (AwaitingType tdest tasks) =
+    "(AwaitingType" <+> pp env tdest <+>
+    vec (hsep $ map (pp env) tasks) <>
+    ")"
+  pp env (ExpandDeclForms _dest _scs waitingOn outScopesDest stx) =
+    "(ExpandDeclForms _" <+> pp env waitingOn <+> pp env outScopesDest <+> pp env stx <> ")"
+  pp env (InterpretMacroAction _dest act konts) =
+    "(InterpretMacroAction" <+>
+    pp env act <+>
+    vec (hsep $ map (pp env) konts) <>
+    ")"
+  pp env (ContinueMacroAction _dest value konts) =
+    "(ContinueMacroAction" <+>
+    pp env value <+>
+    vec (hsep $ map (pp env) konts) <>
+    ")"
+  pp env (EvalDefnAction var name phase _expr) =
+    "(EvalDefnAction" <+> pp env var <+> pp env name <+> pp env phase <> ")"
+  pp env (GeneralizeType e _ _) =
+    "(GeneralizeType" <+> pp env e <+> "_ _)"
+  pp env (ExpandVar t d x v) =
+    "(ExpandVar" <+> pp env t <+> pp env d <+> pp env x <+> pp env v <> ")"
+  pp env (EstablishConstructors _ _ dt _) =
+    "(EstablishConstructors" <+> pp env dt <> ")"
+  pp env (AwaitingPattern _ _ _ _) =
+    "(AwaitingPattern _)"
+  pp env (AwaitingTypePattern _ _ _ _) =
+    "(AwaitingTypePattern _)"
+
+-- SplitCorePtr
+-- PatternPtr
+-- TypePatternPtr
+-- TypeCtorPtr
+
+instance Pretty VarInfo SplitCorePtr where
+  pp _ = viaShow
+
+instance Pretty VarInfo PatternPtr where
+  pp _ = viaShow
+
+instance Pretty VarInfo TypePatternPtr where
+  pp _ = viaShow
+
+instance Pretty VarInfo TypeCtorPtr where
+  pp _ = viaShow
diff --git a/src/ScopeSet.hs b/src/ScopeSet.hs
index c63f4d12..ddf4b53c 100644
--- a/src/ScopeSet.hs
+++ b/src/ScopeSet.hs
@@ -38,7 +38,6 @@ import Data.Typeable
 import Alpha
 import Phase
 import Scope
-import ShortShow
 
 import Util.Store (Store)
 import qualified Util.Store as St
@@ -53,10 +52,6 @@ data ScopeSet = ScopeSet
   deriving (Data, Eq, Ord, Show)
 makeLenses ''ScopeSet
 
-instance ShortShow ScopeSet where
-  shortShow (ScopeSet always phased) =
-    "{" ++ show (Set.toList always) ++ " | " ++ show (St.toList phased) ++ "}"
-
 instance Semigroup ScopeSet where
   scs1 <> scs2 =
     ScopeSet
diff --git a/src/ShortShow.hs b/src/ShortShow.hs
index 07a5419d..927edcab 100644
--- a/src/ShortShow.hs
+++ b/src/ShortShow.hs
@@ -1,39 +1 @@
 module ShortShow where
-
-import Data.Text
-import qualified Data.List as List
-
-import Unique
-
-
-class ShortShow a where
-  shortShow :: a -> String
-
-instance ShortShow Text where
-  shortShow = show
-
-instance ShortShow Unique where
-  shortShow = show . hashUnique
-
-instance (ShortShow a, ShortShow b) => ShortShow (a, b) where
-  shortShow (x, y)
-    = "("
-   ++ shortShow x
-   ++ ", "
-   ++ shortShow y
-   ++ ")"
-instance (ShortShow a, ShortShow b, ShortShow c) => ShortShow (a, b, c) where
-  shortShow (x, y, z)
-    = "("
-   ++ shortShow x
-   ++ ", "
-   ++ shortShow y
-   ++ ", "
-   ++ shortShow z
-   ++ ")"
-
-instance ShortShow a => ShortShow [a] where
-  shortShow xs
-    = "["
-   ++ List.intercalate ", " (fmap shortShow xs)
-   ++ "]"
diff --git a/src/SplitCore.hs b/src/SplitCore.hs
index d010355c..5159807b 100644
--- a/src/SplitCore.hs
+++ b/src/SplitCore.hs
@@ -80,10 +80,25 @@ instance Show TypePatternPtr where
 newTypePatternPtr :: IO TypePatternPtr
 newTypePatternPtr = TypePatternPtr <$> newUnique
 
+newtype TypeCtorPtr = TypeCtorPtr Unique
+  deriving (Eq, Ord)
+
+instance HasKey TypeCtorPtr where
+  getKey (TypeCtorPtr u) = getKey u
+  fromKey i = TypeCtorPtr $! fromKey i
+  {-# INLINE getKey #-}
+  {-# INLINE fromKey #-}
+
+instance Show TypeCtorPtr where
+  show (TypeCtorPtr u) = "(TypeCtorPtr " ++ show (hashUnique u) ++ ")"
+
+newTypeCtorPtr :: IO TypeCtorPtr
+newTypeCtorPtr = TypeCtorPtr <$> newUnique
+
 data SplitCore = SplitCore
   { _splitCoreRoot         :: SplitCorePtr
   , _splitCoreDescendants  :: Store SplitCorePtr (CoreF TypePatternPtr PatternPtr SplitCorePtr)
-  , _splitCorePatterns     :: Store PatternPtr (ConstructorPatternF PatternPtr)
+  , _splitCorePatterns     :: Store PatternPtr (DataPatternF PatternPtr)
   , _splitCoreTypePatterns :: Store TypePatternPtr TypePattern
   }
 makeLenses ''SplitCore
@@ -115,7 +130,7 @@ split partialCore = do
       SplitCorePtr ->
       Maybe (CoreF (Maybe TypePattern) PartialPattern PartialCore) ->
       WriterT (Store SplitCorePtr (CoreF TypePatternPtr PatternPtr SplitCorePtr),
-               Store PatternPtr (ConstructorPatternF PatternPtr),
+               Store PatternPtr (DataPatternF PatternPtr),
                Store TypePatternPtr TypePattern)
         IO
         ()
@@ -133,7 +148,7 @@ split partialCore = do
       PartialPattern ->
       WriterT
         (Store SplitCorePtr (CoreF TypePatternPtr PatternPtr SplitCorePtr),
-         Store PatternPtr (ConstructorPatternF PatternPtr),
+         Store PatternPtr (DataPatternF PatternPtr),
          Store TypePatternPtr TypePattern)
         IO
         PatternPtr
@@ -148,7 +163,7 @@ split partialCore = do
       Maybe TypePattern ->
       WriterT
         (Store SplitCorePtr (CoreF TypePatternPtr PatternPtr SplitCorePtr),
-         Store PatternPtr (ConstructorPatternF PatternPtr),
+         Store PatternPtr (DataPatternF PatternPtr),
          Store TypePatternPtr TypePattern)
         IO
         TypePatternPtr
diff --git a/src/Syntax/SrcLoc.hs b/src/Syntax/SrcLoc.hs
index 9b7ea309..73168372 100644
--- a/src/Syntax/SrcLoc.hs
+++ b/src/Syntax/SrcLoc.hs
@@ -7,7 +7,6 @@ import Control.Lens
 import Data.Data (Data)
 
 import Alpha
-import ShortShow
 
 data SrcPos = SrcPos
   { _srcPosLine :: !Int
@@ -16,9 +15,6 @@ data SrcPos = SrcPos
   deriving (Data, Eq, Show)
 makeLenses ''SrcPos
 
-instance ShortShow SrcPos where
-  shortShow (SrcPos l c) = show l ++ "." ++ show c
-
 data SrcLoc = SrcLoc
   { _srcLocFilePath :: !FilePath
   , _srcLocStart    :: !SrcPos
@@ -29,9 +25,3 @@ makeLenses ''SrcLoc
 
 instance AlphaEq SrcLoc where
   alphaCheck x y = guard (x == y)
-
-instance ShortShow SrcLoc where
-  shortShow (SrcLoc fn beg end) =
-    reverse (take 10 (reverse fn)) ++ ":" ++
-    shortShow beg ++ "-" ++
-    shortShow end
diff --git a/src/Syntax/Syntax.hs b/src/Syntax/Syntax.hs
index b447e613..5bc193ba 100644
--- a/src/Syntax/Syntax.hs
+++ b/src/Syntax/Syntax.hs
@@ -20,7 +20,6 @@ import ModuleName
 import Phase
 import Scope
 import ScopeSet
-import ShortShow
 import Syntax.SrcLoc
 
 import qualified Util.Set   as Set
@@ -109,18 +108,6 @@ instance AlphaEq Syntax where
     alphaCheck x1 x2
 
 
-instance ShortShow a => ShortShow (Stx a) where
-  shortShow (Stx _ _ x) = shortShow x
-
-instance ShortShow a => ShortShow (ExprF a) where
-  shortShow (Id x) = shortShow x
-  shortShow (String s) = show s
-  shortShow (List xs) = shortShow xs
-  shortShow (Integer s) = show s
-
-instance ShortShow Syntax where
-  shortShow (Syntax x) = shortShow x
-
 addScopes' :: HasScopes p => ScopeSet -> p -> p
 #ifndef KDEBUG
 addScopes' scopeSet =  mapScopes (over phaseScopes newSpecificScopes
diff --git a/src/Type.hs b/src/Type.hs
index cc5d377f..0ffb4e00 100644
--- a/src/Type.hs
+++ b/src/Type.hs
@@ -20,7 +20,6 @@ import Numeric.Natural
 import Alpha
 import Datatype
 import Kind
-import ShortShow
 import Unique
 
 import Util.Key
@@ -101,9 +100,6 @@ instance AlphaEq a => AlphaEq (TyF a) where
     guard (length args1 == length args2)
     for_ (zip args1 args2) (uncurry alphaCheck)
 
-instance ShortShow a => ShortShow (TyF a) where
-  shortShow t = show (fmap shortShow t)
-
 
 class TyLike a arg | a -> arg where
   tSyntax     :: a
diff --git a/stdlib/prelude.kl b/stdlib/prelude.kl
index 6de7f4af..16d4c39f 100644
--- a/stdlib/prelude.kl
+++ b/stdlib/prelude.kl
@@ -41,7 +41,7 @@
         ScopeAction flip add remove
         Unit unit
         Bool true false
-        Problem module declaration type expression pattern type-pattern
+        Problem module declaration type expression pattern type-pattern type-constructor
         Maybe nothing just
         List nil ::
         Syntax-Contents list-contents integer-contents string-contents identifier-contents
diff --git a/tests/Test.hs b/tests/Test.hs
index 29f12e90..b6ba8d13 100644
--- a/tests/Test.hs
+++ b/tests/Test.hs
@@ -46,7 +46,6 @@ import Pretty
 import Scope
 import qualified ScopeSet
 import ScopeSet (ScopeSet)
-import ShortShow
 import SplitCore
 import Syntax.SrcLoc
 import Syntax
@@ -608,8 +607,8 @@ genSyntaxError subgen =
   <*> subgen
 
 genLam ::
-  (CoreF TypePattern ConstructorPattern Bool -> GenT IO a) ->
-  GenT IO (CoreF TypePattern ConstructorPattern a)
+  (CoreF TypePattern DataPattern Bool -> GenT IO a) ->
+  GenT IO (CoreF TypePattern DataPattern a)
 genLam subgen = do
   ident <- Gen.generalize genIdent
   var <- genVar
@@ -621,21 +620,21 @@ genLam subgen = do
 -- which subtree of 'CoreF' they're being asked to generate.
 genCoreF ::
   forall a.
-  (Maybe (GenT IO Var) -> CoreF TypePattern ConstructorPattern Bool ->
+  (Maybe (GenT IO Var) -> CoreF TypePattern DataPattern Bool ->
    GenT IO a) {- ^ Generic sub-generator -} ->
   Maybe (GenT IO Var) {- ^ Variable generator -} ->
-  GenT IO (CoreF TypePattern ConstructorPattern a)
+  GenT IO (CoreF TypePattern DataPattern a)
 genCoreF subgen varGen =
   let sameVars = subgen varGen
       -- A unary constructor with no binding
       unary ::
-        (forall b. b -> CoreF TypePattern ConstructorPattern b) ->
-        GenT IO (CoreF TypePattern ConstructorPattern a)
+        (forall b. b -> CoreF TypePattern DataPattern b) ->
+        GenT IO (CoreF TypePattern DataPattern a)
       unary constructor = constructor <$> sameVars (constructor True)
       -- A binary constructor with no binding
       binary ::
-        (forall b. b -> b -> CoreF TypePattern ConstructorPattern b) ->
-        GenT IO (CoreF TypePattern ConstructorPattern a)
+        (forall b. b -> b -> CoreF TypePattern DataPattern b) ->
+        GenT IO (CoreF TypePattern DataPattern a)
       binary constructor =
         constructor
         <$> sameVars (constructor True False)
@@ -653,7 +652,7 @@ genCoreF subgen varGen =
         -- , CoreIdentEq _ <$> sameVars <*> sameVars
         -- , CoreSyntax Syntax
         -- , CoreCase sameVars [(Pattern, core)]
-        -- , CoreDataCase core [(ConstructorPattern, core)]
+        -- , CoreDataCase core [(DataPattern, core)]
         -- , CoreIdent (ScopedIdent core)
         -- , CoreEmpty (ScopedEmpty core)
         -- , CoreCons (ScopedCons core)
diff --git a/toy.kl b/toy.kl
new file mode 100644
index 00000000..826d7b7a
--- /dev/null
+++ b/toy.kl
@@ -0,0 +1,76 @@
+#lang "prelude.kl"
+(import (shift "prelude.kl" 1))
+(import (shift "prelude.kl" 2))
+
+(datatype (T)
+  (mkT))
+
+--(meta
+--  (define-macros
+--    ([my-else
+--      (lambda (_)
+--        (pure '(else _)))])))
+
+--(define-macros
+--  ([my-macro
+--    (lambda (stx)
+--      (>>= (which-problem)
+--        (lambda (problem)
+--          (case problem
+--            [(expression type)
+--             (type-case type
+--               --[(T)
+--               -- (pure '(mkT))]
+--               [(else x)
+--                (type-case x
+--                  [(T)
+--                   (pure '(mkT))]
+--                  [(else _)
+--                   (pure '(mkT))])])]))))]))
+--(example (the (T) (my-macro)))
+
+(define-macros
+  ([my-macro
+    (lambda (stx)
+      (>>= (which-problem)
+        (lambda (problem)
+          (case problem
+            [(expression type)
+             (type-case type
+               [(the-type T)
+                (pure '(mkT))]
+               [(else _)
+                (pure '(mkT))])]))))]))
+(example (the (T) (my-macro)))
+
+
+
+--                           | e | ee | eee | run
+-- (error _)                   p1  p1   p1   p1   (should be p1)
+-- (which-problem) (error _)   p0  p0   p1   p1   (should be p1)
+-- '(mkT)                      p0  p0   p0   p0   (found in p0)
+-- (which-problem) '(mkT)      p0  p0   p1   p1   (found in p0)
+-- (T)                         p1  p1   p1   p1   (found in p0)
+-- (which-problem) (T)         p1  p1   p1   p0   (found in p0)
+-- (which-problem) (else _)    p1  p1   p1   p0   (found in p0)
+
+-- therefore:
+-- [x] eee is needed, we do want the code after (which-problem) to be evaluated and executed at p1.
+-- [ ] eee is incomplete, it should return code from p0, not p1.
+-- [ ] type-case should look at the types from p0, not p1.
+-- [ ] but we can't, because else
+
+---- David thought of this counter-example:
+--(example
+--  (with-unknown-type (String)
+--    (the (-> String String) (lambda (x) 5))))
+--
+--(define-macros
+--  ([my-macro
+--    (lambda (stx)
+--      (>>= (which-problem)
+--        (lambda (problem)
+--          (case problem
+--            [(expression tp)
+--             (pure '(true))]))))]))
+--(example (my-macro my-keyword))