Add holes for expressions in function clauses and inference support (#136)

* Add holes to abstract and micro

* Support trivial implicit arguments

* Support refinement of meta type variables

docs/org/notes/monomorphization.org

@@ -1,6 +1,6 @@
-* Monomorphization
+#+author: Jan Mas Rovira
 
-/By Jan Mais Rovira/
+* Monomorphization
 
  Monomorphization refers to the process of converting polymorphic code to
  monomorphic code (no type variables) through static analysis.

src/MiniJuvix/Syntax/Abstract/Language.hs

@@ -1,6 +1,7 @@
 module MiniJuvix.Syntax.Abstract.Language
   ( module MiniJuvix.Syntax.Abstract.Language,
     module MiniJuvix.Syntax.Concrete.Language,
+    module MiniJuvix.Syntax.Hole,
   )
 where
 
@@ -9,6 +10,7 @@ import MiniJuvix.Syntax.Concrete.Language (BackendItem, ForeignBlock (..), Liter
 import MiniJuvix.Syntax.Concrete.Name qualified as C
 import MiniJuvix.Syntax.Concrete.Scoped.Name qualified as S
 import MiniJuvix.Syntax.Fixity
+import MiniJuvix.Syntax.Hole
 import MiniJuvix.Syntax.Universe
 
 type TopModuleName = S.TopModulePath
@@ -102,6 +104,7 @@ data Expression
   | ExpressionUniverse Universe
   | ExpressionFunction Function
   | ExpressionLiteral LiteralLoc
+  | ExpressionHole Hole
   --- | ExpressionMatch Match
   ---  ExpressionLambda Lambda not supported yet
   deriving stock (Eq, Show)
@@ -109,6 +112,7 @@ data Expression
 instance HasAtomicity Expression where
   atomicity e = case e of
     ExpressionIden {} -> Atom
+    ExpressionHole {} -> Atom
     ExpressionUniverse u -> atomicity u
     ExpressionApplication a -> atomicity a
     ExpressionFunction f -> atomicity f

src/MiniJuvix/Syntax/Abstract/Language/Extra.hs

@@ -26,12 +26,9 @@ smallerPatternVariables = \case
 
 viewApp :: Expression -> (Expression, [Expression])
 viewApp e = case e of
-  ExpressionIden {} -> (e, [])
   ExpressionApplication (Application l r) ->
     second (`snoc` r) (viewApp l)
-  ExpressionUniverse {} -> (e, [])
+  _ -> (e, [])
-  ExpressionFunction {} -> (e, [])
-  ExpressionLiteral {} -> (e, [])
 
 viewExpressionAsPattern :: Expression -> Maybe Pattern
 viewExpressionAsPattern e = case viewApp e of

src/MiniJuvix/Syntax/Abstract/Pretty/Base.hs

@@ -131,6 +131,7 @@ instance PrettyCode Expression where
     ExpressionApplication a -> ppCode a
     ExpressionFunction f -> ppCode f
     ExpressionLiteral l -> ppSCode l
+    ExpressionHole h -> ppSCode h
 
 instance PrettyCode Usage where
   ppCode u = return $ case u of

src/MiniJuvix/Syntax/Concrete/Language.hs

@@ -5,6 +5,7 @@ module MiniJuvix.Syntax.Concrete.Language
     module MiniJuvix.Syntax.Concrete.Name,
     module MiniJuvix.Syntax.Concrete.Scoped.NameRef,
     module MiniJuvix.Syntax.Concrete.Loc,
+    module MiniJuvix.Syntax.Hole,
     module MiniJuvix.Syntax.Concrete.LiteralLoc,
     module MiniJuvix.Syntax.Backends,
     module MiniJuvix.Syntax.ForeignBlock,
@@ -34,6 +35,7 @@ import MiniJuvix.Syntax.Concrete.Scoped.NameRef
 import MiniJuvix.Syntax.Concrete.Scoped.VisibilityAnn
 import MiniJuvix.Syntax.Fixity
 import MiniJuvix.Syntax.ForeignBlock
+import MiniJuvix.Syntax.Hole
 import MiniJuvix.Syntax.Universe
 import MiniJuvix.Syntax.Usage
 import Prelude (show)
@@ -57,6 +59,11 @@ type family IdentifierType s = res | res -> s where
   IdentifierType 'Parsed = Name
   IdentifierType 'Scoped = ScopedIden
 
+type HoleType :: Stage -> GHC.Type
+type family HoleType s = res | res -> s where
+  HoleType 'Parsed = Interval
+  HoleType 'Scoped = Hole
+
 type PatternAtomIdenType :: Stage -> GHC.Type
 type family PatternAtomIdenType s = res | res -> s where
   PatternAtomIdenType 'Parsed = Name
@@ -534,11 +541,13 @@ data Expression
   | ExpressionUniverse Universe
   | ExpressionLiteral LiteralLoc
   | ExpressionFunction (Function 'Scoped)
+  | ExpressionHole (HoleType 'Scoped)
   deriving stock (Show, Eq, Ord)
 
 instance HasAtomicity Expression where
   atomicity e = case e of
     ExpressionIdentifier {} -> Atom
+    ExpressionHole {} -> Atom
     ExpressionParensIdentifier {} -> Atom
     ExpressionApplication {} -> Aggregate appFixity
     ExpressionInfixApplication a -> Aggregate (getFixity a)
@@ -902,6 +911,7 @@ deriving stock instance
 data ExpressionAtom (s :: Stage)
   = AtomIdentifier (IdentifierType s)
   | AtomLambda (Lambda s)
+  | AtomHole (HoleType s)
   | AtomLetBlock (LetBlock s)
   | AtomUniverse Universe
   | AtomFunction (Function s)
@@ -1004,6 +1014,7 @@ deriving stock instance
   ( Show (ExpressionType s),
     Show (IdentifierType s),
     Show (ModuleRefType s),
+    Show (HoleType s),
     Show (SymbolType s),
     Show (PatternType s)
   ) =>
@@ -1012,6 +1023,7 @@ deriving stock instance
 deriving stock instance
   ( Eq (ExpressionType s),
     Eq (IdentifierType s),
+    Eq (HoleType s),
     Eq (ModuleRefType s),
     Eq (SymbolType s),
     Eq (PatternType s)
@@ -1022,6 +1034,7 @@ deriving stock instance
   ( Ord (ExpressionType s),
     Ord (IdentifierType s),
     Ord (ModuleRefType s),
+    Ord (HoleType s),
     Ord (SymbolType s),
     Ord (PatternType s)
   ) =>
@@ -1031,6 +1044,7 @@ deriving stock instance
   ( Show (ExpressionType s),
     Show (IdentifierType s),
     Show (ModuleRefType s),
+    Show (HoleType s),
     Show (SymbolType s),
     Show (PatternType s)
   ) =>
@@ -1050,6 +1064,7 @@ instance
   ( Eq (ExpressionType s),
     Eq (IdentifierType s),
     Eq (ModuleRefType s),
+    Eq (HoleType s),
     Eq (SymbolType s),
     Eq (PatternType s)
   ) =>
@@ -1061,6 +1076,7 @@ instance
   ( Ord (ExpressionType s),
     Ord (IdentifierType s),
     Ord (ModuleRefType s),
+    Ord (HoleType s),
     Ord (SymbolType s),
     Ord (PatternType s)
   ) =>

src/MiniJuvix/Syntax/Concrete/Lexer.hs

@@ -146,6 +146,7 @@ allKeywords =
     kwEval,
     kwForeign,
     kwHiding,
+    kwHole,
     kwImport,
     kwIn,
     kwInductive,
@@ -275,6 +276,9 @@ kwUsing = keyword Str.using
 kwWhere :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r ()
 kwWhere = keyword Str.where_
 
+kwHole :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r ()
+kwHole = keyword Str.underscore
+
 kwWildcard :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r ()
 kwWildcard = keyword Str.underscore
 

src/MiniJuvix/Syntax/Concrete/Parser.hs

@@ -185,6 +185,7 @@ expressionAtom =
     <|> (AtomMatch <$> match)
     <|> (AtomLetBlock <$> letBlock)
     <|> (AtomFunArrow <$ kwRightArrow)
+    <|> (AtomHole <$> hole)
     <|> parens (AtomParens <$> parseExpressionAtoms)
 
 parseExpressionAtoms ::
@@ -194,6 +195,13 @@ parseExpressionAtoms = do
   (_expressionAtoms, _expressionAtomsLoc) <- interval (P.some expressionAtom)
   return ExpressionAtoms {..}
 
+--------------------------------------------------------------------------------
+-- Holes
+--------------------------------------------------------------------------------
+
+hole :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (HoleType 'Parsed)
+hole = snd <$> interval kwHole
+
 --------------------------------------------------------------------------------
 -- Literals
 --------------------------------------------------------------------------------

src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs

@@ -447,14 +447,17 @@ instance PrettyCode Name where
     NameUnqualified s -> ppSymbol s
     NameQualified s -> ppCode s
 
+nameIdSuffix :: Members '[Reader Options] r => S.NameId -> Sem r (Maybe (Doc Ann))
+nameIdSuffix nid = do
+  showNameId <- asks (^. optShowNameId)
+  if
+      | showNameId -> Just . ("@" <>) <$> ppCode nid
+      | otherwise -> return Nothing
+
 instance PrettyCode n => PrettyCode (S.Name' n) where
   ppCode S.Name' {..} = do
     nameConcrete' <- annotateKind _nameKind <$> ppCode _nameConcrete
-    showNameId <- asks (^. optShowNameId)
+    uid <- nameIdSuffix _nameId
-    uid <-
-      if
-          | showNameId -> Just . ("@" <>) <$> ppCode _nameId
-          | otherwise -> return Nothing
     return $ annSRef (nameConcrete' <?> uid)
     where
       annSRef :: Doc Ann -> Doc Ann
@@ -706,6 +709,7 @@ instance PrettyCode ScopedIden where
 instance PrettyCode Expression where
   ppCode e = case e of
     ExpressionIdentifier n -> ppCode n
+    ExpressionHole w -> ppHole w
     ExpressionParensIdentifier n -> parens <$> ppCode n
     ExpressionApplication a -> ppCode a
     ExpressionInfixApplication a -> ppCode a
@@ -783,8 +787,18 @@ ppCodeAtom c = do
   p' <- ppCode c
   return $ if isAtomic c then p' else parens p'
 
+ppHole :: forall s r. (Members '[Reader Options] r, SingI s) => HoleType s -> Sem r (Doc Ann)
+ppHole w = case sing :: SStage s of
+  SParsed -> return kwWildcard
+  SScoped -> ppCode w
+
+instance PrettyCode Hole where
+  ppCode h = do
+    suff <- nameIdSuffix (h ^. holeId)
+    return (kwWildcard <?> suff)
+
 instance SingI s => PrettyCode (ExpressionAtom s) where
-  ppCode a = case a of
+  ppCode = \case
     AtomIdentifier n -> ppName n
     AtomLambda l -> ppCode l
     AtomLetBlock lb -> ppCode lb
@@ -794,6 +808,7 @@ instance SingI s => PrettyCode (ExpressionAtom s) where
     AtomFunArrow -> return kwArrowR
     AtomMatch m -> ppCode m
     AtomParens e -> parens <$> ppExpression e
+    AtomHole w -> ppHole w
 
 instance SingI s => PrettyCode (ExpressionAtoms s) where
   ppCode as = hsep . toList <$> mapM ppCode (as ^. expressionAtoms)

src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs

@@ -1113,9 +1113,22 @@ checkExpressionAtom e = case e of
   AtomFunction fun -> AtomFunction <$> checkFunction fun
   AtomParens par -> AtomParens <$> checkParens par
   AtomFunArrow -> return AtomFunArrow
+  AtomHole h -> AtomHole <$> checkHole h
   AtomLiteral l -> return (AtomLiteral l)
   AtomMatch match -> AtomMatch <$> checkMatch match
 
+checkHole ::
+  Members '[NameIdGen] r =>
+  HoleType 'Parsed ->
+  Sem r Hole
+checkHole h = do
+  i <- freshNameId
+  return
+    Hole
+      { _holeId = i,
+        _holeLoc = h
+      }
+
 checkParens ::
   Members '[Error ScoperError, State Scope, State ScoperState, Reader LocalVars, InfoTableBuilder, NameIdGen] r =>
   ExpressionAtoms 'Parsed ->
@@ -1306,12 +1319,21 @@ parseTerm =
     parseUniverse
       <|> parseNoInfixIdentifier
       <|> parseParens
+      <|> parseHole
       <|> parseFunction
       <|> parseLambda
       <|> parseLiteral
       <|> parseMatch
       <|> parseLetBlock
   where
+    parseHole :: Parse Expression
+    parseHole = ExpressionHole <$> P.token lit mempty
+      where
+        lit :: ExpressionAtom 'Scoped -> Maybe Hole
+        lit s = case s of
+          AtomHole l -> Just l
+          _ -> Nothing
+
     parseLiteral :: Parse Expression
     parseLiteral = ExpressionLiteral <$> P.token lit mempty
       where

src/MiniJuvix/Syntax/Hole.hs

@@ -0,0 +1,28 @@
+module MiniJuvix.Syntax.Hole where
+
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.NameId
+import Prettyprinter
+
+data Hole = Hole
+  { _holeId :: NameId,
+    _holeLoc :: Interval
+  }
+  deriving stock (Show)
+
+makeLenses ''Hole
+
+instance Eq Hole where
+  (==) = (==) `on` (^. holeId)
+
+instance Ord Hole where
+  compare = compare `on` (^. holeId)
+
+instance Hashable Hole where
+  hashWithSalt s = hashWithSalt s . (^. holeId)
+
+instance HasLoc Hole where
+  getLoc = (^. holeLoc)
+
+instance Pretty Hole where
+  pretty = const "_"

src/MiniJuvix/Syntax/MicroJuvix/Language.hs

@@ -3,6 +3,7 @@ module MiniJuvix.Syntax.MicroJuvix.Language
     module MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind,
     module MiniJuvix.Syntax.Concrete.Scoped.Name,
     module MiniJuvix.Syntax.Concrete.Loc,
+    module MiniJuvix.Syntax.Hole,
   )
 where
 
@@ -13,6 +14,7 @@ import MiniJuvix.Syntax.Concrete.Scoped.Name (NameId (..))
 import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
 import MiniJuvix.Syntax.Fixity
 import MiniJuvix.Syntax.ForeignBlock
+import MiniJuvix.Syntax.Hole
 import Prettyprinter
 
 type FunctionName = Name
@@ -122,6 +124,7 @@ data Expression
   | ExpressionApplication Application
   | ExpressionFunction FunctionExpression
   | ExpressionLiteral LiteralLoc
+  | ExpressionHole Hole
   | ExpressionTyped TypedExpression
   deriving stock (Show)
 
@@ -197,6 +200,7 @@ data Type
   | TypeApp TypeApplication
   | TypeFunction Function
   | TypeAbs TypeAbstraction
+  | TypeHole Hole
   | TypeUniverse
   | TypeAny
   deriving stock (Eq, Show, Generic)
@@ -244,6 +248,7 @@ instance HasAtomicity Expression where
     ExpressionTyped t -> atomicity (t ^. typedExpression)
     ExpressionLiteral l -> atomicity l
     ExpressionFunction f -> atomicity f
+    ExpressionHole {} -> Atom
 
 instance HasAtomicity Function where
   atomicity = const (Aggregate funFixity)
@@ -256,6 +261,7 @@ instance HasAtomicity Type where
     TypeIden {} -> Atom
     TypeFunction f -> atomicity f
     TypeUniverse -> Atom
+    TypeHole {} -> Atom
     TypeAny -> Atom
     TypeAbs a -> atomicity a
     TypeApp a -> atomicity a
@@ -281,6 +287,7 @@ instance HasLoc Expression where
     ExpressionTyped t -> getLoc (t ^. typedExpression)
     ExpressionLiteral l -> getLoc l
     ExpressionFunction f -> getLoc f
+    ExpressionHole h -> getLoc h
 
 instance HasLoc Iden where
   getLoc = \case

src/MiniJuvix/Syntax/MicroJuvix/Language/Extra.hs

@@ -5,6 +5,7 @@ module MiniJuvix.Syntax.MicroJuvix.Language.Extra
 where
 
 import Data.HashMap.Strict qualified as HashMap
+import Data.HashSet qualified as HashSet
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.MicroJuvix.Language
 
@@ -98,6 +99,7 @@ mkConcreteType = fmap ConcreteType . go
         r' <- go r
         return (TypeFunction (Function l' r'))
       TypeAbs {} -> Nothing
+      TypeHole {} -> Nothing
       TypeIden i -> case i of
         TypeIdenInductive {} -> return t
         TypeIdenAxiom {} -> return t
@@ -107,6 +109,97 @@ mkConcreteType = fmap ConcreteType . go
 expressionAsType' :: Expression -> Type
 expressionAsType' = fromMaybe impossible . expressionAsType
 
+findHoles :: Type -> HashSet Hole
+findHoles = go
+  where
+    go :: Type -> HashSet Hole
+    go = \case
+      TypeIden {} -> mempty
+      TypeApp (TypeApplication a b) -> go a <> go b
+      TypeFunction (Function a b) -> go a <> go b
+      TypeAbs (TypeAbstraction _ t) -> go t
+      TypeHole h -> HashSet.singleton h
+      TypeUniverse -> mempty
+      TypeAny -> mempty
+
+hasHoles :: Type -> Bool
+hasHoles = not . HashSet.null . findHoles
+
+typeAsExpression :: Type -> Expression
+typeAsExpression = go
+  where
+    go :: Type -> Expression
+    go =
+      \case
+        TypeIden i -> ExpressionIden (goTypeIden i)
+        TypeApp a -> ExpressionApplication (goApp a)
+        TypeFunction f -> ExpressionFunction (goFunction f)
+        TypeAny -> error "TODO TypeAny"
+        TypeAbs {} -> error "TODO TypeAbs"
+        TypeHole h -> ExpressionHole h
+        TypeUniverse -> error "TODO TypeUniverse"
+
+    goTypeIden :: TypeIden -> Iden
+    goTypeIden = \case
+      TypeIdenInductive i -> IdenInductive i
+      TypeIdenAxiom a -> IdenAxiom a
+      TypeIdenVariable v -> IdenVar v
+    goApp :: TypeApplication -> Application
+    goApp (TypeApplication l r) = Application (go l) (go r)
+    goFunction :: Function -> FunctionExpression
+    goFunction (Function l r) = FunctionExpression (go l) (go r)
+
+fillHoles :: HashMap Hole Type -> Expression -> Expression
+fillHoles m = goe
+  where
+    goe :: Expression -> Expression
+    goe x = case x of
+      ExpressionIden {} -> x
+      ExpressionApplication a -> ExpressionApplication (goApp a)
+      ExpressionLiteral {} -> x
+      ExpressionHole h -> goHole h
+      ExpressionFunction f -> ExpressionFunction (goFunction f)
+      ExpressionTyped t ->
+        ExpressionTyped
+          ( over
+              typedType
+              (fillHolesType m)
+              (over typedExpression goe t)
+          )
+      where
+        goApp :: Application -> Application
+        goApp (Application l r) = Application (goe l) (goe r)
+        goFunction :: FunctionExpression -> FunctionExpression
+        goFunction (FunctionExpression l r) = FunctionExpression (goe l) (goe r)
+        goHole :: Hole -> Expression
+        goHole h = case HashMap.lookup h m of
+          Just r -> typeAsExpression r
+          Nothing -> ExpressionHole h
+
+fillHolesType :: HashMap Hole Type -> Type -> Type
+fillHolesType m = go
+  where
+    go :: Type -> Type
+    go = \case
+      TypeIden i -> TypeIden i
+      TypeApp a -> TypeApp (goApp a)
+      TypeAbs a -> TypeAbs (goAbs a)
+      TypeFunction f -> TypeFunction (goFunction f)
+      TypeUniverse -> TypeUniverse
+      TypeAny -> TypeAny
+      TypeHole h -> goHole h
+      where
+        goApp :: TypeApplication -> TypeApplication
+        goApp (TypeApplication l r) = TypeApplication (go l) (go r)
+        goAbs :: TypeAbstraction -> TypeAbstraction
+        goAbs (TypeAbstraction v b) = TypeAbstraction v (go b)
+        goFunction :: Function -> Function
+        goFunction (Function l r) = Function (go l) (go r)
+        goHole :: Hole -> Type
+        goHole h = case HashMap.lookup h m of
+          Just ty -> ty
+          Nothing -> TypeHole h
+
 -- | If the expression is of type TypeUniverse it should return Just.
 expressionAsType :: Expression -> Maybe Type
 expressionAsType = go
@@ -117,6 +210,7 @@ expressionAsType = go
       ExpressionLiteral {} -> Nothing
       ExpressionFunction f -> TypeFunction <$> goFunction f
       ExpressionTyped e -> go (e ^. typedExpression)
+      ExpressionHole h -> Just (TypeHole h)
     goFunction :: FunctionExpression -> Maybe Function
     goFunction (FunctionExpression l r) = do
       l' <- go l
@@ -222,9 +316,10 @@ concreteTypeToExpr = go . (^. unconcreteType)
       TypeAbs {} -> impossible
       TypeIden i -> ExpressionIden (goIden i)
       TypeApp (TypeApplication l r) -> ExpressionApplication (Application (go l) (go r))
-      TypeFunction {} -> error "TODO"
+      TypeFunction (Function l r) -> ExpressionFunction (FunctionExpression (go l) (go r))
       TypeUniverse {} -> impossible
       TypeAny {} -> impossible
+      TypeHole {} -> impossible
     goIden :: TypeIden -> Iden
     goIden = \case
       TypeIdenInductive n -> IdenInductive n
@@ -242,6 +337,7 @@ substitutionE m = go
       ExpressionIden i -> goIden i
       ExpressionApplication a -> ExpressionApplication (goApp a)
       ExpressionLiteral {} -> x
+      ExpressionHole {} -> x
       ExpressionFunction f -> ExpressionFunction (goFunction f)
       ExpressionTyped t -> ExpressionTyped (over typedExpression go t)
     goApp :: Application -> Application
@@ -265,6 +361,7 @@ substitution m = go
       TypeFunction f -> TypeFunction (goFunction f)
       TypeUniverse -> TypeUniverse
       TypeAny -> TypeAny
+      TypeHole h -> TypeHole h
     goApp :: TypeApplication -> TypeApplication
     goApp (TypeApplication l r) = TypeApplication (go l) (go r)
     goAbs :: TypeAbstraction -> TypeAbstraction
@@ -319,12 +416,10 @@ unfoldApplication (Application l' r') = second (|: r') (unfoldExpression l')
   where
     unfoldExpression :: Expression -> (Expression, [Expression])
     unfoldExpression e = case e of
-      ExpressionIden {} -> (e, [])
       ExpressionApplication (Application l r) ->
         second (`snoc` r) (unfoldExpression l)
-      ExpressionLiteral {} -> (e, [])
-      ExpressionFunction {} -> (e, [])
       ExpressionTyped t -> unfoldExpression (t ^. typedExpression)
+      _ -> (e, [])
 
 unfoldTypeApplication :: TypeApplication -> (Type, NonEmpty Type)
 unfoldTypeApplication (TypeApplication l' r') = second (|: r') (unfoldType l')

src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs

@@ -75,6 +75,7 @@ instance PrettyCode FunctionExpression where
 instance PrettyCode Expression where
   ppCode = \case
     ExpressionIden i -> ppCode i
+    ExpressionHole h -> ppCode h
     ExpressionApplication a -> ppCode a
     ExpressionTyped a -> ppCode a
     ExpressionFunction f -> ppCode f
@@ -119,6 +120,9 @@ kwColonColon = keyword (Str.colon <> Str.colon)
 kwPipe :: Doc Ann
 kwPipe = keyword Str.pipe
 
+kwHole :: Doc Ann
+kwHole = keyword Str.underscore
+
 kwAxiom :: Doc Ann
 kwAxiom = keyword Str.axiom
 
@@ -167,6 +171,9 @@ instance PrettyCode FunctionArgType where
     FunctionArgTypeType t -> ppCode t
     FunctionArgTypeAbstraction v -> ppCode v
 
+instance PrettyCode Hole where
+  ppCode _ = return kwHole
+
 instance PrettyCode Type where
   ppCode = \case
     TypeIden i -> ppCode i
@@ -175,6 +182,7 @@ instance PrettyCode Type where
     TypeAny -> return kwAny
     TypeApp a -> ppCode a
     TypeAbs a -> ppCode a
+    TypeHole h -> ppCode h
 
 instance PrettyCode InductiveConstructorDef where
   ppCode c = do

src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs

@@ -14,6 +14,7 @@ import MiniJuvix.Syntax.MicroJuvix.Language.Extra
 import MiniJuvix.Syntax.MicroJuvix.LocalVars
 import MiniJuvix.Syntax.MicroJuvix.MicroJuvixResult
 import MiniJuvix.Syntax.MicroJuvix.MicroJuvixTypedResult
+import MiniJuvix.Syntax.MicroJuvix.TypeChecker.Inference
 
 entryMicroJuvixTyped ::
   Member (Error TypeCheckerError) r =>
@@ -84,14 +85,14 @@ checkFunctionDef FunctionDef {..} = do
       }
 
 checkExpression ::
-  Members '[Reader InfoTable, Error TypeCheckerError, Reader LocalVars] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError, Reader LocalVars, Inference] r =>
   Type ->
   Expression ->
   Sem r Expression
 checkExpression t e = do
   e' <- inferExpression' e
   let inferredType = e' ^. typedType
-  unless (matchTypes t inferredType) (throw (err inferredType))
+  unlessM (matchTypes t inferredType) (throw (err inferredType))
   return (ExpressionTyped e')
   where
     err infTy =
@@ -103,59 +104,8 @@ checkExpression t e = do
             }
         )
 
-matchTypes ::
-  Type ->
-  Type ->
-  Bool
-matchTypes a b =
-  isAny a || isAny b || alphaEq a b
-  where
-    isAny = \case
-      TypeAny -> True
-      _ -> False
-
--- | Alpha equivalence
-alphaEq :: Type -> Type -> Bool
-alphaEq ty = run . runReader ini . go ty
-  where
-    ini :: HashMap VarName VarName
-    ini = mempty
-    go ::
-      forall r.
-      Members '[Reader (HashMap VarName VarName)] r =>
-      Type ->
-      Type ->
-      Sem r Bool
-    go a' b' = case (a', b') of
-      (TypeIden a, TypeIden b) -> goIden a b
-      (TypeApp a, TypeApp b) -> goApp a b
-      (TypeAbs a, TypeAbs b) -> goAbs a b
-      (TypeFunction a, TypeFunction b) -> goFunction a b
-      (TypeUniverse, TypeUniverse) -> return True
-      -- TODO TypeAny should match anything?
-      (TypeAny, TypeAny) -> return True
-      -- TODO is the final wildcard bad style?
-      -- what if more Type constructors are added
-      _ -> return False
-      where
-        goIden :: TypeIden -> TypeIden -> Sem r Bool
-        goIden ia ib = case (ia, ib) of
-          (TypeIdenInductive a, TypeIdenInductive b) -> return (a == b)
-          (TypeIdenAxiom a, TypeIdenAxiom b) -> return (a == b)
-          (TypeIdenVariable a, TypeIdenVariable b) -> do
-            mappedEq <- (== Just b) . HashMap.lookup a <$> ask
-            return (a == b || mappedEq)
-          _ -> return False
-        goApp :: TypeApplication -> TypeApplication -> Sem r Bool
-        goApp (TypeApplication f x) (TypeApplication f' x') = andM [go f f', go x x']
-        goFunction :: Function -> Function -> Sem r Bool
-        goFunction (Function l r) (Function l' r') = andM [go l l', go r r']
-        goAbs :: TypeAbstraction -> TypeAbstraction -> Sem r Bool
-        goAbs (TypeAbstraction v1 r) (TypeAbstraction v2 r') =
-          local (HashMap.insert v1 v2) (go r r')
-
 inferExpression ::
-  Members '[Reader InfoTable, Error TypeCheckerError, Reader LocalVars] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError, Reader LocalVars, Inference] r =>
   Expression ->
   Sem r Expression
 inferExpression = fmap ExpressionTyped . inferExpression'
@@ -190,6 +140,15 @@ constructorArgTypes i =
     i ^. constructorInfoArgs
   )
 
+checkFunctionClauseBody ::
+  Members '[Reader InfoTable, Error TypeCheckerError] r =>
+  LocalVars ->
+  Type ->
+  Expression ->
+  Sem r Expression
+checkFunctionClauseBody locals expectedTy body =
+  runInference (runReader locals (checkExpression expectedTy body))
+
 checkFunctionClause ::
   Members '[Reader InfoTable, Error TypeCheckerError] r =>
   FunctionInfo ->
@@ -210,8 +169,7 @@ checkFunctionClause info clause@FunctionClause {..} = do
                       (locals ^. localTyMap)
                   )
                   bodyTy
-          _clauseBody' <-
+          _clauseBody' <- checkFunctionClauseBody locals bodyTy' _clauseBody
-            runReader locals (checkExpression bodyTy' _clauseBody)
           return
             FunctionClause
               { _clauseBody = _clauseBody',
@@ -310,7 +268,7 @@ checkPattern funName = go
 
 inferExpression' ::
   forall r.
-  Members '[Reader InfoTable, Reader LocalVars, Error TypeCheckerError] r =>
+  Members '[Reader InfoTable, Reader LocalVars, Error TypeCheckerError, Inference] r =>
   Expression ->
   Sem r TypedExpression
 inferExpression' e = case e of
@@ -319,6 +277,7 @@ inferExpression' e = case e of
   ExpressionTyped t -> return t
   ExpressionLiteral l -> goLiteral l
   ExpressionFunction f -> goExpressionFunction f
+  ExpressionHole h -> freshMetavar h
   where
     goExpressionFunction :: FunctionExpression -> Sem r TypedExpression
     goExpressionFunction (FunctionExpression l r) = do
@@ -412,8 +371,4 @@ viewTypeApp :: Type -> (Type, [Type])
 viewTypeApp t = case t of
   TypeApp (TypeApplication l r) ->
     second (`snoc` r) (viewTypeApp l)
-  TypeAny {} -> (t, [])
+  _ -> (t, [])
-  TypeUniverse {} -> (t, [])
-  TypeAbs {} -> (t, [])
-  TypeFunction {} -> (t, [])
-  TypeIden {} -> (t, [])

src/MiniJuvix/Syntax/MicroJuvix/TypeChecker/Inference.hs

@@ -0,0 +1,160 @@
+module MiniJuvix.Syntax.MicroJuvix.TypeChecker.Inference where
+
+import Data.HashMap.Strict qualified as HashMap
+import MiniJuvix.Prelude hiding (fromEither)
+import MiniJuvix.Syntax.MicroJuvix.Error
+import MiniJuvix.Syntax.MicroJuvix.Language.Extra
+
+data MetavarState
+  = Fresh
+  | -- | Type may contain holes
+    Refined Type
+
+data Inference m a where
+  FreshMetavar :: Hole -> Inference m TypedExpression
+  MatchTypes :: Type -> Type -> Inference m Bool
+
+makeSem ''Inference
+
+newtype InferenceState = InferenceState
+  { _inferenceMap :: HashMap Hole MetavarState
+  }
+
+makeLenses ''InferenceState
+
+iniState :: InferenceState
+iniState = InferenceState mempty
+
+closeState :: Member (Error TypeCheckerError) r => InferenceState -> Sem r (HashMap Hole Type)
+closeState = \case
+  InferenceState m -> execState mempty (f m)
+  where
+    f ::
+      forall r'.
+      Members '[Error TypeCheckerError, State (HashMap Hole Type)] r' =>
+      HashMap Hole MetavarState ->
+      Sem r' ()
+    f m = mapM_ (uncurry goHole) (HashMap.toList m)
+      where
+        goHole :: Hole -> MetavarState -> Sem r' Type
+        goHole h = \case
+          Fresh -> throw @TypeCheckerError (error "unsolved meta")
+          Refined t -> do
+            s <- gets @(HashMap Hole Type) (^. at h)
+            case s of
+              Just noHolesTy -> return noHolesTy
+              Nothing -> do
+                x <- goType t
+                modify (HashMap.insert h x)
+                return x
+        goType :: Type -> Sem r' Type
+        goType t = case t of
+          TypeIden {} -> return t
+          TypeApp (TypeApplication a b) -> do
+            a' <- goType a
+            b' <- goType b
+            return (TypeApp (TypeApplication a' b'))
+          TypeFunction (Function a b) -> do
+            a' <- goType a
+            b' <- goType b
+            return (TypeFunction (Function a' b'))
+          TypeAbs (TypeAbstraction v b) -> TypeAbs . TypeAbstraction v <$> goType b
+          TypeUniverse -> return TypeUniverse
+          TypeAny -> return TypeAny
+          TypeHole h' ->
+            let st = fromJust (m ^. at h')
+             in goHole h' st
+
+getMetavar :: Member (State InferenceState) r => Hole -> Sem r MetavarState
+getMetavar h = gets (fromJust . (^. inferenceMap . at h))
+
+re :: Member (Error TypeCheckerError) r => Sem (Inference ': r) Expression -> Sem (State InferenceState ': r) Expression
+re = reinterpret $ \case
+  FreshMetavar h -> freshMetavar' h
+  MatchTypes a b -> matchTypes' a b
+  where
+    queryMetavar' :: Members '[State InferenceState] r => Hole -> Sem r (Maybe Type)
+    queryMetavar' h = metavarType <$> getMetavar h
+
+    freshMetavar' :: Members '[State InferenceState] r => Hole -> Sem r TypedExpression
+    freshMetavar' h = do
+      modify (over inferenceMap (HashMap.insert h Fresh))
+      return
+        TypedExpression
+          { _typedExpression = ExpressionHole h,
+            _typedType = TypeUniverse
+          }
+
+    refineMetavar' ::
+      Members '[Error TypeCheckerError, State InferenceState] r =>
+      Hole ->
+      Type ->
+      Sem r ()
+    refineMetavar' h t = do
+      s <- gets (fromJust . (^. inferenceMap . at h))
+      case s of
+        Fresh -> modify (over inferenceMap (HashMap.insert h (Refined t)))
+        Refined r -> goRefine r t
+
+    goRefine :: Members '[Error TypeCheckerError, State InferenceState] r => Type -> Type -> Sem r ()
+    goRefine r t = do
+      eq <- matchTypes' r t
+      unless eq (error "type error: cannot match types")
+
+    metavarType :: MetavarState -> Maybe Type
+    metavarType = \case
+      Fresh -> Nothing
+      Refined t -> Just t
+
+    -- Supports alpha equivalence.
+    matchTypes' :: Members '[Error TypeCheckerError, State InferenceState] r => Type -> Type -> Sem r Bool
+    matchTypes' ty = runReader ini . go ty
+      where
+        ini :: HashMap VarName VarName
+        ini = mempty
+        go ::
+          forall r.
+          Members '[Error TypeCheckerError, State InferenceState, Reader (HashMap VarName VarName)] r =>
+          Type ->
+          Type ->
+          Sem r Bool
+        go a' b' = case (a', b') of
+          (TypeIden a, TypeIden b) -> goIden a b
+          (TypeApp a, TypeApp b) -> goApp a b
+          (TypeAbs a, TypeAbs b) -> goAbs a b
+          (TypeFunction a, TypeFunction b) -> goFunction a b
+          (TypeUniverse, TypeUniverse) -> return True
+          (TypeAny, _) -> return True
+          (_, TypeAny) -> return True
+          (TypeHole h, a) -> goHole h a
+          (a, TypeHole h) -> goHole h a
+          -- TODO is the final wildcard bad style?
+          -- what if more Type constructors are added
+          _ -> return False
+          where
+            goHole :: Hole -> Type -> Sem r Bool
+            goHole h t = do
+              r <- queryMetavar' h
+              case r of
+                Nothing -> refineMetavar' h t $> True
+                Just ht -> matchTypes' t ht
+            goIden :: TypeIden -> TypeIden -> Sem r Bool
+            goIden ia ib = case (ia, ib) of
+              (TypeIdenInductive a, TypeIdenInductive b) -> return (a == b)
+              (TypeIdenAxiom a, TypeIdenAxiom b) -> return (a == b)
+              (TypeIdenVariable a, TypeIdenVariable b) -> do
+                mappedEq <- (== Just b) . HashMap.lookup a <$> ask
+                return (a == b || mappedEq)
+              _ -> return False
+            goApp :: TypeApplication -> TypeApplication -> Sem r Bool
+            goApp (TypeApplication f x) (TypeApplication f' x') = andM [go f f', go x x']
+            goFunction :: Function -> Function -> Sem r Bool
+            goFunction (Function l r) (Function l' r') = andM [go l l', go r r']
+            goAbs :: TypeAbstraction -> TypeAbstraction -> Sem r Bool
+            goAbs (TypeAbstraction v1 r) (TypeAbstraction v2 r') =
+              local (HashMap.insert v1 v2) (go r r')
+
+runInference :: Member (Error TypeCheckerError) r => Sem (Inference ': r) Expression -> Sem r Expression
+runInference a = do
+  (subs, expr) <- runState iniState (re a) >>= firstM closeState
+  return (fillHoles subs expr)

src/MiniJuvix/Termination/Checker.hs

@@ -94,6 +94,7 @@ checkExpression e =
       ExpressionApplication a -> checkApplication a
       ExpressionFunction f -> checkFunction f
       ExpressionIden {} -> return ()
+      ExpressionHole {} -> return ()
       ExpressionUniverse {} -> return ()
       ExpressionLiteral {} -> return ()
 

src/MiniJuvix/Translation/AbstractToMicroJuvix.hs

@@ -215,6 +215,7 @@ goType e = case e of
   Abstract.ExpressionApplication a -> TypeApp <$> goTypeApplication a
   Abstract.ExpressionFunction f -> goFunction f
   Abstract.ExpressionLiteral {} -> unsupported "literals in types"
+  Abstract.ExpressionHole h -> return (TypeHole h)
 
 goApplication :: Abstract.Application -> Sem r Application
 goApplication (Abstract.Application f x) = do
@@ -249,6 +250,7 @@ goExpression e = case e of
   Abstract.ExpressionFunction f -> ExpressionFunction <$> goExpressionFunction f
   Abstract.ExpressionApplication a -> ExpressionApplication <$> goApplication a
   Abstract.ExpressionLiteral l -> return (ExpressionLiteral l)
+  Abstract.ExpressionHole h -> return (ExpressionHole h)
 
 goInductiveParameter :: Abstract.FunctionParameter -> Sem r InductiveParameter
 goInductiveParameter f =
@@ -302,6 +304,7 @@ viewConstructorType :: Abstract.Expression -> Sem r ([Type], Type)
 viewConstructorType e = case e of
   Abstract.ExpressionFunction f -> first toList <$> viewFunctionType f
   Abstract.ExpressionIden i -> return ([], TypeIden (goTypeIden i))
+  Abstract.ExpressionHole {} -> unsupported "holes in constructor type"
   Abstract.ExpressionApplication a -> do
     a' <- goTypeApplication a
     return ([], TypeApp a')

src/MiniJuvix/Translation/MicroJuvixToMonoJuvix.hs

@@ -292,6 +292,7 @@ goExpression = go
       Micro.ExpressionTyped t -> go (t ^. Micro.typedExpression)
       Micro.ExpressionApplication a -> goApp a
       Micro.ExpressionFunction {} -> impossible
+      Micro.ExpressionHole {} -> impossible
     goApp :: Micro.Application -> Sem r Expression
     goApp a = do
       let (f, args) = Micro.unfoldApplication a
@@ -499,6 +500,7 @@ goType = go . (^. Micro.unconcreteType)
       Micro.TypeAny -> return TypeAny
       Micro.TypeUniverse -> return TypeUniverse
       Micro.TypeAbs {} -> impossible
+      Micro.TypeHole {} -> impossible
       Micro.TypeFunction f -> TypeFunction <$> goFunction f
       Micro.TypeApp a -> goApp a
     goApp :: Micro.TypeApplication -> Sem r Type

src/MiniJuvix/Translation/MicroJuvixToMonoJuvix/TypeCallsMapBuilder.hs

@@ -97,6 +97,7 @@ goType = \case
   TypeIden {} -> return ()
   TypeApp a -> goTypeApplication a
   TypeAny -> return ()
+  TypeHole {} -> impossible
   TypeUniverse -> return ()
   TypeFunction f -> goFunction f
   TypeAbs a -> goTypeAbstraction a
@@ -115,6 +116,7 @@ goExpression = \case
   ExpressionApplication a -> goApplication a
   ExpressionFunction a -> goFunctionExpression a
   ExpressionLiteral {} -> return ()
+  ExpressionHole {} -> impossible
   ExpressionTyped t -> do
     goType (t ^. typedType)
     goExpression (t ^. typedExpression)

src/MiniJuvix/Translation/ScopedToAbstract.hs

@@ -182,12 +182,13 @@ goExpression = \case
   ExpressionApplication a -> A.ExpressionApplication <$> goApplication a
   ExpressionInfixApplication ia -> A.ExpressionApplication <$> goInfix ia
   ExpressionPostfixApplication pa -> A.ExpressionApplication <$> goPostfix pa
-  ExpressionLiteral l -> return $ A.ExpressionLiteral l
+  ExpressionLiteral l -> return (A.ExpressionLiteral l)
   ExpressionLambda {} -> unsupported "Lambda"
   ExpressionMatch {} -> unsupported "Match"
   ExpressionLetBlock {} -> unsupported "Let Block"
   ExpressionUniverse uni -> return $ A.ExpressionUniverse (goUniverse uni)
   ExpressionFunction func -> A.ExpressionFunction <$> goFunction func
+  ExpressionHole h -> return (A.ExpressionHole h)
   where
     goIden :: C.ScopedIden -> A.Expression
     goIden x = A.ExpressionIden $ case x of

test/BackendC/Positive.hs

@@ -125,5 +125,6 @@ tests =
     PosTest "Inductive types and pattern matching" "Nat",
     PosTest "Polymorphic types" "Polymorphism",
     PosTest "Multiple modules" "MultiModules",
-    PosTest "Higher Order Functions" "HigherOrder"
+    PosTest "Higher Order Functions" "HigherOrder",
+    PosTest "Higher Order Functions and explicit holes" "PolymorphismHoles"
   ]

test/MonoJuvix/Positive.hs

@@ -38,5 +38,9 @@ tests =
     PosTest
       "Polymorphic Simple Fungible Token"
       "FullExamples"
-      "PolySimpleFungibleToken.mjuvix"
+      "PolySimpleFungibleToken.mjuvix",
+    PosTest
+      "Polymorphism and higher rank functions with explicit holes"
+      "."
+      "PolymorphismHoles.mjuvix"
   ]

test/TypeCheck/Positive.hs

@@ -47,6 +47,10 @@ tests =
       "GHC backend Hello World"
       "MiniHaskell"
       "HelloWorld.mjuvix",
+    PosTest
+      "PolySimpleFungibleToken with explicit holes"
+      "FullExamples"
+      "PolySimpleFungibleTokenHoles.mjuvix",
     PosTest
       "GHC backend MonoSimpleFungibleToken"
       "FullExamples"
@@ -66,5 +70,9 @@ tests =
     PosTest
       "Polymorphism and higher rank functions"
       "."
-      "Polymorphism.mjuvix"
+      "Polymorphism.mjuvix",
+    PosTest
+      "Polymorphism and higher rank functions with explicit holes"
+      "."
+      "PolymorphismHoles.mjuvix"
   ]

tests/positive/FullExamples/PolySimpleFungibleTokenHoles.mjuvix

@@ -0,0 +1,303 @@
+module PolySimpleFungibleTokenHoles;
+
+foreign ghc {
+  import Anoma
+};
+
+--------------------------------------------------------------------------------
+-- Booleans
+--------------------------------------------------------------------------------
+
+inductive Bool {
+  true : Bool;
+  false : Bool;
+};
+
+infixr 2 ||;
+|| : Bool → Bool → Bool;
+|| false a ≔ a;
+|| true _ ≔ true;
+
+infixr 3 &&;
+&& : Bool → Bool → Bool;
+&& false _ ≔ false;
+&& true a ≔ a;
+
+if : (A : Type) → Bool → A → A → A;
+if _ true a _ ≔ a;
+if _ false _ b ≔ b;
+
+--------------------------------------------------------------------------------
+-- Backend Booleans
+--------------------------------------------------------------------------------
+
+axiom BackendBool : Type;
+
+compile BackendBool {
+  ghc ↦ "Bool";
+};
+
+axiom backend-true : BackendBool;
+compile backend-true {
+  ghc ↦ "True";
+};
+
+axiom backend-false : BackendBool;
+compile backend-false {
+  ghc ↦ "False";
+};
+
+--------------------------------------------------------------------------------
+-- Backend Bridge
+--------------------------------------------------------------------------------
+
+foreign ghc {
+  bool :: Bool -> a -> a -> a
+  bool True x _ = x
+  bool False _ y = y
+};
+
+axiom bool : BackendBool → Bool → Bool → Bool;
+compile bool {
+  ghc ↦ "bool";
+};
+
+from-backend-bool : BackendBool → Bool;
+from-backend-bool bb ≔ bool bb true false;
+
+--------------------------------------------------------------------------------
+-- Functions
+--------------------------------------------------------------------------------
+
+const : (A : Type) → (B : Type) → A → B → A;
+const _ _ a _ ≔ a;
+
+id : (A : Type) → A → A;
+id _ a ≔ a;
+
+--------------------------------------------------------------------------------
+-- Integers
+--------------------------------------------------------------------------------
+
+axiom Int : Type;
+compile Int {
+  ghc ↦ "Int";
+};
+
+infix 4 <';
+axiom <' : Int → Int → BackendBool;
+compile <' {
+  ghc ↦ "(<)";
+};
+
+infix 4 <;
+< : Int → Int → Bool;
+< i1 i2 ≔ from-backend-bool (i1 <' i2);
+
+axiom eqInt : Int → Int → BackendBool;
+compile eqInt {
+  ghc ↦ "(==)";
+};
+
+infix 4 ==Int;
+==Int : Int → Int → Bool;
+==Int i1 i2 ≔ from-backend-bool (eqInt i1 i2);
+
+infixl 6 -;
+axiom - : Int -> Int -> Int;
+compile - {
+  ghc ↦ "(-)";
+};
+
+infixl 6 +;
+axiom + : Int -> Int -> Int;
+compile + {
+  ghc ↦ "(+)";
+};
+
+--------------------------------------------------------------------------------
+-- Strings
+--------------------------------------------------------------------------------
+
+axiom String : Type;
+compile String {
+  ghc ↦ "[Char]";
+};
+
+axiom eqString : String → String → BackendBool;
+compile eqString  {
+  ghc ↦ "(==)";
+};
+
+infix 4 ==String;
+==String : String → String → Bool;
+==String s1 s2 ≔ from-backend-bool (eqString s1 s2);
+
+--------------------------------------------------------------------------------
+-- Lists
+--------------------------------------------------------------------------------
+
+inductive List (A : Type) {
+  nil : List A;
+  cons : A → List A → List A;
+};
+
+elem : (A : Type) → (A → A → Bool) → A → List A → Bool;
+elem _ _ _ nil ≔ false;
+elem _ eq s (cons x xs) ≔ eq s x || elem _ eq s xs;
+
+foldl : (A : Type) → (B : Type) → (B → A → B) → B → List A → B;
+foldl _ _ f z nil ≔ z;
+foldl _ _ f z (cons h hs) ≔ foldl _ _ f (f z h) hs;
+
+--------------------------------------------------------------------------------
+-- Pair
+--------------------------------------------------------------------------------
+
+inductive Pair (A : Type) (B : Type) {
+  mkPair : A → B → Pair A B;
+};
+
+--------------------------------------------------------------------------------
+-- Maybe
+--------------------------------------------------------------------------------
+
+inductive Maybe (A : Type) {
+ nothing : Maybe A;
+ just : A → Maybe A;
+};
+
+from-int : Int → Maybe Int;
+from-int i ≔ if _ (i < 0) (nothing _) (just _ i);
+
+maybe : (A : Type) → (B : Type) → B → (A → B) → Maybe A → B;
+maybe _ _ b _ nothing ≔ b;
+maybe _ _ _ f (just x) ≔ f x;
+
+from-string : String → Maybe String;
+from-string s ≔ if _ (s ==String "") (nothing _) (just _ s);
+
+pair-from-optionString : (String → Pair Int Bool) → Maybe String → Pair Int Bool;
+pair-from-optionString ≔ maybe _ _ (mkPair _ _ 0 false);
+
+--------------------------------------------------------------------------------
+-- Anoma
+--------------------------------------------------------------------------------
+
+axiom readPre : String → Int;
+compile readPre {
+  ghc ↦ "readPre";
+};
+
+axiom readPost : String → Int;
+compile readPost {
+  ghc ↦ "readPost";
+};
+
+axiom isBalanceKey : String → String → String;
+compile isBalanceKey {
+  ghc ↦ "isBalanceKey";
+};
+
+read-pre : String → Maybe Int;
+read-pre s ≔ from-int (readPre s);
+
+read-post : String → Maybe Int;
+read-post s ≔ from-int (readPost s);
+
+is-balance-key : String → String → Maybe String;
+is-balance-key token key ≔ from-string (isBalanceKey token key);
+
+unwrap-default : Maybe Int → Int;
+unwrap-default o ≔ maybe _ _ 0 (id _) o;
+
+--------------------------------------------------------------------------------
+-- Validity Predicate
+--------------------------------------------------------------------------------
+
+change-from-key : String → Int;
+change-from-key key ≔ unwrap-default (read-post key) - unwrap-default (read-pre key);
+
+check-vp : List String → String → Int → String → Pair Int Bool;
+check-vp verifiers key change owner ≔
+    if _
+        (change-from-key key < 0)
+        -- make sure the spender approved the transaction
+        (mkPair _ _ (change + (change-from-key key)) (elem _ (==String) owner verifiers))
+        (mkPair _ _ (change + (change-from-key key)) true);
+
+check-keys : String → List String → Pair Int Bool → String → Pair Int Bool;
+check-keys token verifiers (mkPair change is-success) key ≔
+    if _
+        is-success
+        (pair-from-optionString (check-vp verifiers key change) (is-balance-key token key))
+        (mkPair _ _ 0 false);
+
+check-result : Pair Int Bool → Bool;
+check-result (mkPair change all-checked) ≔ (change ==Int 0) && all-checked;
+
+vp : String → List String → List String → Bool;
+vp token keys-changed verifiers ≔
+    check-result
+        (foldl _ _
+            (check-keys token verifiers)
+            (mkPair _ _ 0 true)
+            keys-changed);
+
+--------------------------------------------------------------------------------
+-- IO
+--------------------------------------------------------------------------------
+
+axiom Action : Type;
+compile Action {
+ ghc ↦ "IO ()";
+};
+
+axiom putStr : String → Action;
+compile putStr {
+  ghc ↦ "putStr";
+};
+
+axiom putStrLn : String → Action;
+compile putStrLn {
+  ghc ↦ "putStrLn";
+};
+
+infixl 1 >>;
+axiom >> : Action → Action → Action;
+compile >> {
+  ghc ↦ "(>>)";
+};
+
+show-result : Bool → String;
+show-result true ≔ "OK";
+show-result false ≔ "FAIL";
+
+--------------------------------------------------------------------------------
+-- Testing VP
+--------------------------------------------------------------------------------
+
+token : String;
+token ≔ "owner-token";
+
+owner-address : String;
+owner-address ≔ "owner-address";
+
+change1-key : String;
+change1-key ≔ "change1-key";
+
+change2-key : String;
+change2-key ≔ "change2-key";
+
+verifiers : List String;
+verifiers ≔ cons _ owner-address (nil _);
+
+keys-changed : List String;
+keys-changed ≔ cons _ change1-key (cons _ change2-key (nil _));
+
+main : Action;
+main ≔
+    (putStr "VP Status: ")
+    >> (putStrLn (show-result (vp token keys-changed verifiers)));
+
+end;

tests/positive/MiniC/PolymorphismHoles/Input.mjuvix

@@ -0,0 +1,89 @@
+module Input;
+
+--------------------------------------------------------------------------------
+-- Booleans
+--------------------------------------------------------------------------------
+
+inductive Bool {
+  true : Bool;
+  false : Bool;
+};
+
+--------------------------------------------------------------------------------
+-- Strings
+--------------------------------------------------------------------------------
+
+axiom String : Type;
+
+compile String {
+  ghc ↦ "[Char]";
+  c ↦ "char*";
+};
+
+--------------------------------------------------------------------------------
+-- IO
+--------------------------------------------------------------------------------
+
+axiom Action : Type;
+
+compile Action {
+  ghc ↦ "IO ()";
+  c ↦ "int";
+};
+
+foreign c {
+  int sequence(int a, int b) {
+    return a + b;
+  \}
+};
+
+infixl 1 >>;
+axiom >> : Action → Action → Action;
+
+compile >> {
+  ghc ↦ "(>>)";
+  c ↦ "sequence";
+};
+
+axiom put-str : String → Action;
+
+compile put-str {
+  ghc ↦ "putStr";
+  c ↦ "putStr";
+};
+
+axiom put-str-ln : String → Action;
+
+compile put-str-ln {
+  ghc ↦ "putStrLn";
+  c ↦ "putStrLn";
+};
+
+bool-to-str : Bool → String;
+bool-to-str true ≔ "True";
+bool-to-str false ≔ "False";
+
+
+--------------------------------------------------------------------------------
+-- Pair
+--------------------------------------------------------------------------------
+
+inductive Pair (A : Type) (B : Type) {
+ mkPair : A → B → Pair A B;
+};
+
+fst : (A : Type) → (B : Type) → Pair A B → A;
+fst _ _ (mkPair a b) ≔ a;
+
+--------------------------------------------------------------------------------
+-- Main
+--------------------------------------------------------------------------------
+
+fst-of-pair : Action;
+fst-of-pair ≔ (put-str "fst (True, False) = ")
+               >> put-str-ln (bool-to-str (fst _ _ (mkPair _ _ true false)));
+
+main : Action;
+main ≔ fst-of-pair;
+
+end;

tests/positive/MiniC/PolymorphismHoles/expected.golden

@@ -0,0 +1 @@
+fst (True, False) = True

tests/positive/PolymorphismHoles.mjuvix

@@ -0,0 +1,105 @@
+module PolymorphismHoles;
+
+inductive Pair (A : Type) (B : Type) {
+ mkPair : A → B → Pair A B;
+};
+
+inductive Nat {
+ zero : Nat;
+ suc : Nat → Nat;
+};
+
+inductive List (A : Type) {
+ nil : List A;
+ -- TODO check that the return type is saturated with the proper variable
+ cons : A → List A → Nat;
+};
+
+inductive Bool {
+ false : Bool;
+ true : Bool;
+};
+
+id : (A : Type) → A → A;
+id _ a ≔ a;
+
+terminating
+undefined : (A : Type) → A;
+undefined A ≔ undefined A;
+
+add : Nat → Nat → Nat;
+add zero b ≔ b;
+add (suc a) b ≔ suc (add a b);
+
+nil' : (E : Type) → List E;
+nil' A ≔ nil _;
+
+-- currying
+nil'' : (E : Type) → List E;
+nil'' ≔ nil;
+
+fst : (A : Type) → (B : Type) → Pair A B → A;
+fst _ _ (mkPair a b) ≔ a;
+
+p : Pair Bool Bool;
+p ≔ mkPair _ _ true false;
+
+swap : (A : Type) → (B : Type) → Pair A B → Pair B A;
+swap A B (mkPair a b) ≔ mkPair _ _ b a;
+
+curry : (A : Type) → (B : Type) → (C : Type)
+  → (Pair A B → C) → A → B → C;
+curry A B C f a b ≔ f (mkPair _ _ a b) ;
+
+ap : (A : Type) → (B : Type)
+  → (A → B) → A → B;
+ap A B f a ≔ f a;
+
+headDef : (A : Type) → A → List A → A;
+headDef _ d nil ≔ d;
+headDef A _ (cons h _) ≔ h;
+
+ite : (A : Type) → Bool → A → A → A;
+ite _ true tt _ ≔ tt;
+ite _ false _ ff ≔ ff;
+
+filter : (A : Type) → (A → Bool) → List A → List A;
+filter _ f nil ≔ nil _;
+filter _ f (cons x xs) ≔ ite _ (f x) (cons _ x (filter _ f xs)) (filter _ f xs);
+
+map : (A : Type) → (B : Type) →
+  (A → B) → List A → List B;
+map _ _ f nil ≔ nil _;
+map _ _ f (cons x xs) ≔ cons _ (f x) (map _ _ f xs);
+
+zip : (A : Type) → (B : Type)
+    → List A → List B → List (Pair A B);
+zip A _ nil _ ≔ nil _;
+zip _ _ _ nil ≔ nil _;
+zip _ _ (cons a as) (cons b bs) ≔ nil _;
+
+zipWith : (A : Type) → (B : Type) → (C : Type)
+  → (A → B → C)
+  → List A → List B → List C;
+zipWith _ _ C f nil _ ≔ nil C;
+zipWith _ _ C f _ nil ≔ nil C;
+zipWith _ _ _ f (cons a as) (cons b bs) ≔ cons _ (f a b) (zipWith _ _ _ f as bs);
+
+rankn : ((A : Type) → A → A) → Bool → Nat → Pair Bool Nat;
+rankn f b n ≔ mkPair _ _ (f _ b) (f _ n);
+
+-- currying
+trankn : Pair Bool Nat;
+trankn ≔ rankn id false zero;
+
+l1 : List Nat;
+l1 ≔ cons _ zero (nil _);
+
+pairEval : (A : Type) → (B : Type) → Pair (A → B) A → B;
+pairEval _ _ (mkPair f x) ≔ f x;
+
+main : Nat;
+main ≔ headDef _ (pairEval _ _ (mkPair _ _ (add zero) zero))
+   (zipWith _ _ _ add l1 l1);
+
+end;