Remove ExpressionTyped from MicroJuvix language (#143)

src/MiniJuvix/Syntax/MicroJuvix/ArityChecker.hs

@@ -108,7 +108,6 @@ guessArity ::
   Expression ->
   Sem r (Maybe Arity)
 guessArity = \case
-  ExpressionTyped {} -> impossible
   ExpressionHole {} -> return Nothing
   ExpressionFunction {} -> return (Just ArityUnit)
   ExpressionLiteral {} -> return (Just arityLiteral)
@@ -142,7 +141,6 @@ guessArity = \case
           ExpressionApplication {} -> impossible
           ExpressionFunction {} -> return (Just ArityUnit)
           ExpressionLiteral {} -> return (Just arityLiteral)
-          ExpressionTyped {} -> impossible
           ExpressionIden i -> idenHelper i
 
 -- | The arity of all literals is assumed to be: {} -> 1
@@ -324,7 +322,6 @@ checkExpression hintArity expr = case expr of
   ExpressionLiteral {} -> appHelper expr []
   ExpressionFunction {} -> return expr
   ExpressionHole {} -> return expr
-  ExpressionTyped {} -> impossible
   where
     goApp :: Application -> Sem r Expression
     goApp = uncurry appHelper . second toList . unfoldApplication'
@@ -344,7 +341,6 @@ checkExpression hintArity expr = case expr of
                   }
             )
         ExpressionApplication {} -> impossible
-        ExpressionTyped {} -> impossible
       return (foldApplication fun args')
       where
         helper :: Interval -> Arity -> Sem r [(IsImplicit, Expression)]

src/MiniJuvix/Syntax/MicroJuvix/Language.hs

@@ -126,7 +126,6 @@ data Expression
   | ExpressionFunction FunctionExpression
   | ExpressionLiteral LiteralLoc
   | ExpressionHole Hole
-  | ExpressionTyped TypedExpression
 
 data Application = Application
   { _appLeft :: Expression,
@@ -244,7 +243,6 @@ instance HasAtomicity Expression where
   atomicity e = case e of
     ExpressionIden {} -> Atom
     ExpressionApplication a -> atomicity a
-    ExpressionTyped t -> atomicity (t ^. typedExpression)
     ExpressionLiteral l -> atomicity l
     ExpressionFunction f -> atomicity f
     ExpressionHole {} -> Atom
@@ -283,7 +281,6 @@ instance HasLoc Expression where
   getLoc = \case
     ExpressionIden i -> getLoc i
     ExpressionApplication a -> getLoc (a ^. appLeft)
-    ExpressionTyped t -> getLoc (t ^. typedExpression)
     ExpressionLiteral l -> getLoc l
     ExpressionFunction f -> getLoc f
     ExpressionHole h -> getLoc h

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

@@ -167,13 +167,6 @@ fillHoles m = goe
       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 i) = Application (goe l) (goe r) i
@@ -216,7 +209,6 @@ expressionAsType = go
       ExpressionApplication a -> TypeApp <$> goApp a
       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
@@ -346,7 +338,6 @@ substitutionE m = go
       ExpressionLiteral {} -> x
       ExpressionHole {} -> x
       ExpressionFunction f -> ExpressionFunction (goFunction f)
-      ExpressionTyped t -> ExpressionTyped (over typedExpression go t)
     goApp :: Application -> Application
     goApp (Application l r i) = Application (go l) (go r) i
     goFunction :: FunctionExpression -> FunctionExpression
@@ -431,7 +422,6 @@ unfoldApplication' (Application l' r' i') = second (|: (i', r')) (unfoldExpressi
     unfoldExpression e = case e of
       ExpressionApplication (Application l r i) ->
         second (`snoc` (i, r)) (unfoldExpression l)
-      ExpressionTyped t -> unfoldExpression (t ^. typedExpression)
       _ -> (e, [])
 
 unfoldApplication :: Application -> (Expression, NonEmpty Expression)

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

@@ -81,7 +81,6 @@ instance PrettyCode Expression where
     ExpressionIden i -> ppCode i
     ExpressionHole h -> ppCode h
     ExpressionApplication a -> ppCode a
-    ExpressionTyped a -> ppCode a
     ExpressionFunction f -> ppCode f
     ExpressionLiteral l -> return (pretty l)
 

src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs

@@ -112,7 +112,7 @@ checkExpression expectedTy e = do
   e' <- inferExpression' e
   let inferredType = e' ^. typedType
   unlessM (matchTypes expectedTy inferredType) (throw (err inferredType))
-  return (ExpressionTyped e')
+  return (e' ^. typedExpression)
   where
     err infTy =
       ErrWrongType
@@ -127,7 +127,7 @@ inferExpression ::
   Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference] r =>
   Expression ->
   Sem r Expression
-inferExpression = fmap ExpressionTyped . inferExpression'
+inferExpression = fmap (^. typedExpression) . inferExpression'
 
 lookupVar :: Member (Reader LocalVars) r => Name -> Sem r Type
 lookupVar v = HashMap.lookupDefault impossible v <$> asks (^. localTypes)
@@ -288,7 +288,6 @@ inferExpression' ::
 inferExpression' e = case e of
   ExpressionIden i -> inferIden i
   ExpressionApplication a -> inferApplication a
-  ExpressionTyped t -> return t
   ExpressionLiteral l -> goLiteral l
   ExpressionFunction f -> goExpressionFunction f
   ExpressionHole h -> freshMetavar h
@@ -332,7 +331,7 @@ inferExpression' e = case e of
                 { _typedExpression =
                     ExpressionApplication
                       Application
-                        { _appLeft = ExpressionTyped l,
+                        { _appLeft = l ^. typedExpression,
                           _appRight = r,
                           _appImplicit = i
                         },
@@ -346,7 +345,7 @@ inferExpression' e = case e of
                 { _typedExpression =
                     ExpressionApplication
                       Application
-                        { _appLeft = ExpressionTyped l,
+                        { _appLeft = l ^. typedExpression,
                           _appRight = r,
                           _appImplicit = i
                         },
@@ -372,7 +371,7 @@ inferExpression' e = case e of
                       _typedExpression =
                         ExpressionApplication
                           Application
-                            { _appLeft = ExpressionTyped l,
+                            { _appLeft = l ^. typedExpression,
                               _appRight = r,
                               _appImplicit = i
                             }

src/MiniJuvix/Translation/MicroJuvixToMonoJuvix.hs

@@ -289,7 +289,6 @@ goExpression = go
     go = \case
       Micro.ExpressionIden i -> return (ExpressionIden (goIden i))
       Micro.ExpressionLiteral l -> return (ExpressionLiteral l)
-      Micro.ExpressionTyped t -> go (t ^. Micro.typedExpression)
       Micro.ExpressionApplication a -> goApp a
       Micro.ExpressionFunction {} -> impossible
       Micro.ExpressionHole {} -> impossible

src/MiniJuvix/Translation/MicroJuvixToMonoJuvix/TypeCallsMapBuilder.hs

@@ -116,9 +116,6 @@ goExpression = \case
   ExpressionFunction a -> goFunctionExpression a
   ExpressionLiteral {} -> return ()
   ExpressionHole {} -> impossible
-  ExpressionTyped t -> do
-    goType (t ^. typedType)
-    goExpression (t ^. typedExpression)
 
 goApplication :: Members '[State TypeCallsMap, Reader Caller, Reader InfoTable] r => Application -> Sem r ()
 goApplication a = do
@@ -137,6 +134,8 @@ goApplication a = do
             { _typeCallIden = FunctionIden fun,
               _typeCallArguments = tyArgs
             }
+    -- Note: cosntructors do not need to be checked as they are already covered
+    -- by inspecting the types
     _ -> return ()
   where
     take' :: Int -> NonEmpty a -> NonEmpty a

tests/positive/MiniC/Polymorphism/Input.mjuvix

@@ -63,17 +63,17 @@ 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;
+infixr 2 ×;
+infixr 4 ,;
+inductive × (A : Type) (B : Type) {
+  , : A → B → A × B;
 };
 
-fst : (A : Type) → (B : Type) → Pair A B → A;
-fst _ _ (mkPair a b) ≔ a;
+fst : {A : Type} → {B : Type} → A × B → A;
+fst (a , b) ≔ a;
+
+id' : {A : Type} → A → A;
+id' a ≔ fst (a , a);
 
 --------------------------------------------------------------------------------
 -- Main
@@ -81,9 +81,9 @@ fst _ _ (mkPair a b) ≔ a;
 
 fst-of-pair : Action;
 fst-of-pair ≔ (put-str "fst (True, False) = ")
-               >> put-str-ln (bool-to-str (fst Bool Bool (mkPair true false)));
+               >> put-str-ln (bool-to-str (fst (true , false)));
 
 main : Action;
-main ≔ fst-of-pair;
+main ≔ fst-of-pair >> put-str-ln (bool-to-str (id' false));
 
 end;

tests/positive/MiniC/Polymorphism/expected.golden

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