Add with-unknown-type

examples/unknown-type.golden

@@ -0,0 +1,4 @@
+(nothing) : ∀α. (Maybe α)
+(just #[unknown-type.kl:24.33-24.37]<here>) : (Maybe Syntax)
+(just #<closure>) : ∀α. (Maybe (α → α))
+(pair (just #<closure>) (nothing)) : ∀α. (Pair (Maybe (α → α)) (Maybe (α → α)))

examples/unknown-type.kl

@@ -0,0 +1,28 @@
+#lang "n-ary-app.kl"
+
+(import (shift "n-ary-app.kl" 1))
+(import (shift "quasiquote.kl" 1))
+(import "pair-datatype.kl")
+
+(define-macros
+  ([gotta-be-maybe
+    (lambda (stx)
+      (syntax-case stx
+        [(list (_ e))
+         (pure (quasiquote/loc stx (with-unknown-type (A) (the (Maybe A) ,e))))]))]
+   [gotta-be-maybes
+    (lambda (stx)
+      (syntax-case stx
+        [(list (_ e1 e2))
+         (pure
+          (quasiquote/loc stx
+            (with-unknown-type (A)
+              (pair (the (Maybe A) ,e1)
+                    (the (Maybe A) ,e2)))))]))]))
+
+(example (gotta-be-maybe (nothing)))
+(example (gotta-be-maybe (just 'here)))
+(example (gotta-be-maybe (just (lambda (x) x))))
+
+
+(example (gotta-be-maybes (just (lambda (x) x)) (nothing)))

src/Expander.hs

@@ -370,6 +370,8 @@ initializeKernel = do
   traverse_ (uncurry addTypePrimitive) typePrims
   traverse_ (uncurry addPatternPrimitive) patternPrims
   traverse_ addDatatypePrimitive datatypePrims
+  addUniversalPrimitive "with-unknown-type" Prims.makeLocalType
+
 
   where
     typePrims :: [(Text, (SplitTypePtr -> Syntax -> Expand (), TypePatternPtr -> Syntax -> Expand ()))]
@@ -545,6 +547,13 @@ initializeKernel = do
       bind b val
       addToKernel name runtime b
 
+    addUniversalPrimitive :: Text -> (MacroDest -> Syntax -> Expand ()) -> Expand ()
+    addUniversalPrimitive name impl = do
+      let val = EPrimUniversalMacro impl
+      b <- freshBinding
+      bind b val
+      addToKernel name runtime b
+
 
 -- TODO Make import spec language extensible and use bindings rather
 -- than literals
@@ -982,6 +991,8 @@ expandOneForm prob stx
         EPrimPatternMacro impl -> do
           dest <- requirePatternCtx stx prob
           impl dest stx
+        EPrimUniversalMacro impl ->
+          impl prob stx
         EVarMacro var -> do
           (t, dest) <- requireExpressionCtx stx prob
           case syntaxE stx of

src/Expander/Monad.hs

@@ -213,12 +213,14 @@ newtype ExpansionEnv = ExpansionEnv (Map.Map Binding EValue)
   deriving (Semigroup, Monoid)
 
 data EValue
-  = EPrimExprMacro (Ty -> SplitCorePtr -> Syntax -> Expand ()) -- ^ For special forms
+  = EPrimExprMacro (Ty -> SplitCorePtr -> Syntax -> Expand ())
+    -- ^ For special forms
   | EPrimTypeMacro (SplitTypePtr -> Syntax -> Expand ()) (TypePatternPtr -> Syntax -> Expand ())
     -- ^ For type-level special forms - first as types, then as type patterns
   | EPrimModuleMacro (Syntax -> Expand ())
   | EPrimDeclMacro (DeclTreePtr -> DeclOutputScopesPtr -> Syntax -> Expand ())
   | EPrimPatternMacro (Either (Ty, Ty, PatternPtr) (Ty, TypePatternPtr) -> Syntax -> Expand ())
+  | EPrimUniversalMacro (MacroDest -> Syntax -> Expand ())
   | EVarMacro !Var -- ^ For bound variables (the Unique is the binding site of the var)
   | ETypeVar !Natural -- ^ For bound type variables (user-written Skolem variables or in datatype definitions)
   | EUserMacro !MacroVar -- ^ For user-written macros

src/Expander/Primitives.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RankNTypes #-}
@@ -49,6 +50,8 @@ module Expander.Primitives
   , elsePattern
   -- * Module primitives
   , makeModule
+  -- * Anywhere primitives
+  , makeLocalType
   -- * Local primitives
   , prepareVar
   ) where
@@ -539,6 +542,29 @@ makeModule expandDeclForms stx =
 
       pure ()
 
+--------------
+-- Anywhere --
+--------------
+
+makeLocalType :: MacroDest -> Syntax -> Expand ()
+makeLocalType dest stx = do
+  Stx _ _ (_ :: Syntax, binder, body) <- mustHaveEntries stx
+  Stx _ _ theVar <- mustHaveEntries binder
+  (sc, n, b) <- varPrepHelper theVar
+  t <- TMetaVar <$> freshMeta
+
+  let tyImpl tdest tstx = do
+        _ <- mustBeIdent tstx
+        linkType tdest t
+  let patImpl _ tstx =
+        throwError $ NotValidType tstx
+
+  p <- currentPhase
+  addLocalBinding n b
+  bind b $ EPrimTypeMacro tyImpl patImpl
+
+  forkExpandSyntax dest (addScope p body sc)
+
 --------------
 -- Patterns --
 --------------

stdlib/n-ary-app.kl

@@ -98,6 +98,7 @@
 (export #%module #%app
         lambda define example define-macros quote meta
         the -> Syntax Macro
+        with-unknown-type
         if true false
         error
         let flet
@@ -108,4 +109,5 @@
         free-identifier=? bound-identifier=? log make-introducer
         Unit unit
         ScopeAction flip add remove
+        Maybe just nothing
         datatype case else)