Type checking fails when the type of a pattern is not given by the signature (#1378)

* infer hole in type from pattern

* refactor

* fix error message

* format

* fix matching of identifiers

* improve error message

src/Juvix/Syntax/MicroJuvix/Error/Types.hs

@@ -9,8 +9,8 @@ import Juvix.Syntax.MicroJuvix.Language
 -- not match the type of the inductive being matched
 data WrongConstructorType = WrongConstructorType
   { _wrongCtorTypeName :: Name,
-    _wrongCtorTypeExpected :: InductiveName,
-    _wrongCtorTypeActual :: InductiveName,
+    _wrongCtorTypeExpected :: Name,
+    _wrongCtorTypeActual :: Name,
     _wrongCtorTypeFunName :: Name
   }
 
@@ -29,11 +29,11 @@ instance ToGenericError WrongConstructorType where
       msg =
         "The constructor"
           <+> ppCode ctorName
-          <+> "has type:"
+          <+> "belongs to the inductive type:"
             <> line
             <> indent' (ppCode (e ^. wrongCtorTypeActual))
             <> line
-            <> "but is expected to have type:"
+            <> "but is expected to belong to the inductive type:"
             <> line
             <> indent' (ppCode (e ^. wrongCtorTypeExpected))
 
@@ -132,9 +132,9 @@ instance ToGenericError WrongConstructorAppArgs where
 
 -- | the type of an expression does not match the inferred type
 data WrongType = WrongType
-  { _wrongTypeExpression :: Expression,
-    _wrongTypeExpectedType :: Expression,
-    _wrongTypeInferredType :: Expression
+  { _wrongTypeThing :: Either Expression Pattern,
+    _wrongTypeExpected :: Expression,
+    _wrongTypeActual :: Expression
   }
 
 makeLenses ''WrongType
@@ -147,24 +147,24 @@ instance ToGenericError WrongType where
         _genericErrorIntervals = [i]
       }
     where
-      i = getLoc (e ^. wrongTypeExpression)
+      i = either getLoc getLoc (e ^. wrongTypeThing)
       msg =
-        "Type error near"
-          <+> pretty (getLoc subjectExpr)
-            <> "."
-            <> line
-            <> "The expression"
-          <+> ppCode subjectExpr
+        "The"
+          <+> thing
+          <+> either ppCode ppCode subjectThing
           <+> "has type:"
             <> line
-            <> indent' (ppCode (e ^. wrongTypeInferredType))
+            <> indent' (ppCode (e ^. wrongTypeActual))
             <> line
             <> "but is expected to have type:"
             <> line
-            <> indent' (ppCode (e ^. wrongTypeExpectedType))
-
-      subjectExpr :: Expression
-      subjectExpr = e ^. wrongTypeExpression
+            <> indent' (ppCode (e ^. wrongTypeExpected))
+      thing :: Doc a
+      thing = case subjectThing of
+        Left {} -> "expression"
+        Right {} -> "pattern"
+      subjectThing :: Either Expression Pattern
+      subjectThing = e ^. wrongTypeThing
 
 -- | The left hand expression of a function application is not
 -- a function type.

src/Juvix/Syntax/MicroJuvix/TypeChecker.hs

@@ -99,15 +99,15 @@ checkExpression ::
 checkExpression expectedTy e = do
   e' <- inferExpression' e
   let inferredType = e' ^. typedType
-  unlessM (matchTypes expectedTy inferredType) (throw (err inferredType))
+  whenJustM (matchTypes expectedTy inferredType) (throw . err)
   return (e' ^. typedExpression)
   where
-    err infTy =
+    err matchErr =
       ErrWrongType
         ( WrongType
-            { _wrongTypeExpression = e,
-              _wrongTypeInferredType = infTy,
-              _wrongTypeExpectedType = expectedTy
+            { _wrongTypeThing = Left e,
+              _wrongTypeActual = matchErr ^. matchErrorRight,
+              _wrongTypeExpected = matchErr ^. matchErrorLeft
             }
         )
 
@@ -165,7 +165,7 @@ checkFunctionClause info FunctionClause {..} = do
               }
 
 checkPatterns ::
-  Members '[Reader InfoTable, Error TypeCheckerError] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError, Inference, NameIdGen] r =>
   FunctionName ->
   [(FunctionParameter, Pattern)] ->
   Sem r LocalVars
@@ -176,7 +176,7 @@ typeOfArg = (^. paramType)
 
 checkPattern ::
   forall r.
-  Members '[Reader InfoTable, Error TypeCheckerError, State LocalVars] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError, State LocalVars, Inference, NameIdGen] r =>
   FunctionName ->
   FunctionParameter ->
   Pattern ->
@@ -186,11 +186,12 @@ checkPattern funName = go
     go :: FunctionParameter -> Pattern -> Sem r ()
     go argTy p = do
       tyVarMap <- fmap (ExpressionIden . IdenVar) . (^. localTyMap) <$> get
-      let ty = substitutionE tyVarMap (typeOfArg argTy)
-          unbrace = \case
+      ty <- normalizeType (substitutionE tyVarMap (typeOfArg argTy))
+      let unbrace = \case
             PatternBraces b -> b
             x -> x
-      case unbrace p of
+          pat = unbrace p
+      case pat of
         PatternWildcard {} -> return ()
         PatternBraces {} -> impossible
         PatternVariable v -> do
@@ -200,17 +201,48 @@ checkPattern funName = go
               modify (over localTyMap (HashMap.insert v' v))
             _ -> return ()
         PatternConstructorApp a -> do
-          (ind, tyArgs) <- checkSaturatedInductive ty
+          s <- checkSaturatedInductive ty
           info <- lookupConstructor (a ^. constrAppConstructor)
-          let constrInd = info ^. constructorInfoInductive
-          when
-            (ind /= constrInd)
-            ( throw
-                ( ErrWrongConstructorType
-                    (WrongConstructorType (a ^. constrAppConstructor) ind constrInd funName)
+          let constrIndName = info ^. constructorInfoInductive
+              constrName = a ^. constrAppConstructor
+              err :: MatchError -> Sem r ()
+              err m =
+                throw
+                  ( ErrWrongType
+                      WrongType
+                        { _wrongTypeThing = Right pat,
+                          _wrongTypeExpected = m ^. matchErrorRight,
+                          _wrongTypeActual = m ^. matchErrorLeft
+                        }
+                  )
+          case s of
+            Left hole -> do
+              let indParams = info ^. constructorInfoInductiveParameters
+                  numIndParams = length indParams
+                  indName :: Iden
+                  indName = IdenInductive (info ^. constructorInfoInductive)
+                  loc = getLoc a
+              paramHoles <- map ExpressionHole <$> replicateM numIndParams (freshHole loc)
+              let patternTy = foldApplication (ExpressionIden indName) (zip (repeat Explicit) paramHoles)
+              whenJustM
+                (matchTypes patternTy (ExpressionHole hole))
+                err
+              let tyArgs = zipExact indParams paramHoles
+              goConstr a tyArgs
+            Right (ind, tyArgs) -> do
+              when
+                (ind /= constrIndName)
+                ( throw
+                    ( ErrWrongConstructorType
+                        WrongConstructorType
+                          { _wrongCtorTypeName = constrName,
+                            _wrongCtorTypeExpected = ind,
+                            _wrongCtorTypeActual = constrIndName,
+                            _wrongCtorTypeFunName = funName
+                          }
+                    )
                 )
-            )
-          goConstr a tyArgs
+              goConstr a tyArgs
       where
         goConstr :: ConstructorApp -> [(InductiveParameter, Expression)] -> Sem r ()
         goConstr app@(ConstructorApp c ps) ctx = do
@@ -230,39 +262,42 @@ checkPattern funName = go
                     }
                 )
             )
-    checkSaturatedInductive :: Expression -> Sem r (InductiveName, [(InductiveParameter, Expression)])
+    checkSaturatedInductive :: Expression -> Sem r (Either Hole (InductiveName, [(InductiveParameter, Expression)]))
     checkSaturatedInductive ty = do
-      (ind, args) <- viewInductiveApp ty
-      params <-
-        (^. inductiveInfoDef . inductiveParameters)
-          <$> lookupInductive ind
-      let numArgs = length args
-          numParams = length params
-      when
-        (numArgs < numParams)
-        ( throw
-            ( ErrTooFewArgumentsIndType
-                ( WrongNumberArgumentsIndType
-                    { _wrongNumberArgumentsIndTypeActualType = ty,
-                      _wrongNumberArgumentsIndTypeActualNumArgs = numArgs,
-                      _wrongNumberArgumentsIndTypeExpectedNumArgs = numParams
-                    }
+      i <- viewInductiveApp ty
+      case i of
+        Left hole -> return (Left hole)
+        Right (ind, args) -> do
+          params :: [InductiveParameter] <-
+            (^. inductiveInfoDef . inductiveParameters)
+              <$> lookupInductive ind
+          let numArgs = length args
+              numParams = length params
+          when
+            (numArgs < numParams)
+            ( throw
+                ( ErrTooFewArgumentsIndType
+                    ( WrongNumberArgumentsIndType
+                        { _wrongNumberArgumentsIndTypeActualType = ty,
+                          _wrongNumberArgumentsIndTypeActualNumArgs = numArgs,
+                          _wrongNumberArgumentsIndTypeExpectedNumArgs = numParams
+                        }
+                    )
                 )
             )
-        )
-      when
-        (numArgs > numParams)
-        ( throw
-            ( ErrTooManyArgumentsIndType
-                ( WrongNumberArgumentsIndType
-                    { _wrongNumberArgumentsIndTypeActualType = ty,
-                      _wrongNumberArgumentsIndTypeActualNumArgs = numArgs,
-                      _wrongNumberArgumentsIndTypeExpectedNumArgs = numParams
-                    }
+          when
+            (numArgs > numParams)
+            ( throw
+                ( ErrTooManyArgumentsIndType
+                    ( WrongNumberArgumentsIndType
+                        { _wrongNumberArgumentsIndTypeActualType = ty,
+                          _wrongNumberArgumentsIndTypeActualNumArgs = numArgs,
+                          _wrongNumberArgumentsIndTypeExpectedNumArgs = numParams
+                        }
+                    )
                 )
             )
-        )
-      return (ind, zip params args)
+          return (Right (ind, zipExact params args))
 
 freshHole :: Members '[Inference, NameIdGen] r => Interval -> Sem r Hole
 freshHole l = do
@@ -375,7 +410,7 @@ inferExpression' e = case e of
                 r' <- checkExpression (smallUniverse (getLoc h)) r
                 h' <- freshHole (getLoc h)
                 let fun = Function (unnamedParameter r') (ExpressionHole h')
-                unlessM (matchTypes (ExpressionHole h) (ExpressionFunction fun)) impossible
+                whenJustM (matchTypes (ExpressionHole h) (ExpressionFunction fun)) impossible
                 return
                   TypedExpression
                     { _typedType = ExpressionHole h',
@@ -400,11 +435,16 @@ inferExpression' e = case e of
                   )
 
 viewInductiveApp ::
-  Member (Error TypeCheckerError) r =>
+  Members '[Error TypeCheckerError, Inference] r =>
   Expression ->
-  Sem r (InductiveName, [Expression])
+  Sem r (Either Hole (InductiveName, [Expression]))
 viewInductiveApp ty = case t of
-  ExpressionIden (IdenInductive n) -> return (n, as)
+  ExpressionIden (IdenInductive n) -> return (Right (n, as))
+  ExpressionHole h -> do
+    r <- queryMetavar h
+    case r of
+      Just h' -> viewInductiveApp h'
+      Nothing -> return (Left h)
   _ -> throw (ErrImpracticalPatternMatching (ImpracticalPatternMatching ty))
   where
     (t, as) = viewTypeApp ty

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

@@ -10,10 +10,18 @@ data MetavarState
   | -- | Type may contain holes
     Refined Expression
 
+data MatchError = MatchError
+  { _matchErrorLeft :: Expression,
+    _matchErrorRight :: Expression
+  }
+
+makeLenses ''MatchError
+
 data Inference m a where
   FreshMetavar :: Hole -> Inference m TypedExpression
-  MatchTypes :: Expression -> Expression -> Inference m Bool
+  MatchTypes :: Expression -> Expression -> Inference m (Maybe MatchError)
   QueryMetavar :: Hole -> Inference m (Maybe Expression)
+  NormalizeType :: Expression -> Inference m Expression
 
 makeSem ''Inference
 
@@ -61,11 +69,36 @@ closeState = \case
 getMetavar :: Member (State InferenceState) r => Hole -> Sem r MetavarState
 getMetavar h = gets (fromJust . (^. inferenceMap . at h))
 
+normalizeType' :: forall r. Members '[State InferenceState] r => Expression -> Sem r Expression
+normalizeType' = go
+  where
+    go :: Expression -> Sem r Expression
+    go e = case e of
+      ExpressionIden {} -> return e
+      ExpressionHole h -> goHole h
+      ExpressionApplication a -> ExpressionApplication <$> goApp a
+      ExpressionLiteral {} -> return e
+      ExpressionUniverse {} -> return e
+      ExpressionFunction f -> ExpressionFunction <$> goFun f
+    goApp :: Application -> Sem r Application
+    goApp = traverseOf appLeft go >=> traverseOf appRight go
+    goFunPar :: FunctionParameter -> Sem r FunctionParameter
+    goFunPar = traverseOf paramType go
+    goFun :: Function -> Sem r Function
+    goFun = traverseOf functionLeft goFunPar >=> traverseOf functionRight go
+    goHole :: Hole -> Sem r Expression
+    goHole h = do
+      s <- getMetavar h
+      case s of
+        Fresh -> return (ExpressionHole h)
+        Refined r -> go r
+
 re :: Member (Error TypeCheckerError) r => Sem (Inference ': r) a -> Sem (State InferenceState ': r) a
 re = reinterpret $ \case
   FreshMetavar h -> freshMetavar' h
   MatchTypes a b -> matchTypes' a b
   QueryMetavar h -> queryMetavar' h
+  NormalizeType t -> normalizeType' t
   where
     queryMetavar' :: Members '[State InferenceState] r => Hole -> Sem r (Maybe Expression)
     queryMetavar' h = do
@@ -98,7 +131,7 @@ re = reinterpret $ \case
               Refined {} -> impossible
 
     -- Supports alpha equivalence.
-    matchTypes' :: Members '[Error TypeCheckerError, State InferenceState] r => Expression -> Expression -> Sem r Bool
+    matchTypes' :: Members '[Error TypeCheckerError, State InferenceState] r => Expression -> Expression -> Sem r (Maybe MatchError)
     matchTypes' ty = runReader ini . go ty
       where
         ini :: HashMap VarName VarName
@@ -108,41 +141,58 @@ re = reinterpret $ \case
           Members '[Error TypeCheckerError, State InferenceState, Reader (HashMap VarName VarName)] r =>
           Expression ->
           Expression ->
-          Sem r Bool
+          Sem r (Maybe MatchError)
         go a' b' = case (a', b') of
           (ExpressionIden a, ExpressionIden b) -> goIden a b
           (ExpressionApplication a, ExpressionApplication b) -> goApplication a b
           (ExpressionFunction a, ExpressionFunction b) -> goFunction a b
-          (ExpressionUniverse u, ExpressionUniverse u') -> return (u == u')
+          (ExpressionUniverse u, ExpressionUniverse u') -> check (u == u')
           (ExpressionHole h, a) -> goHole h a
           (a, ExpressionHole h) -> goHole h a
-          (ExpressionIden {}, _) -> return False
-          (_, ExpressionIden {}) -> return False
-          (ExpressionApplication {}, _) -> return False
-          (_, ExpressionApplication {}) -> return False
-          (ExpressionFunction {}, _) -> return False
-          (_, ExpressionFunction {}) -> return False
-          (ExpressionUniverse {}, _) -> return False
-          (_, ExpressionUniverse {}) -> return False
-          (ExpressionLiteral l, ExpressionLiteral l') -> return (l == l')
+          (ExpressionIden {}, _) -> err
+          (_, ExpressionIden {}) -> err
+          (ExpressionApplication {}, _) -> err
+          (_, ExpressionApplication {}) -> err
+          (ExpressionFunction {}, _) -> err
+          (_, ExpressionFunction {}) -> err
+          (ExpressionUniverse {}, _) -> err
+          (_, ExpressionUniverse {}) -> err
+          (ExpressionLiteral l, ExpressionLiteral l') -> check (l == l')
           where
-            goHole :: Hole -> Expression -> Sem r Bool
+            ok :: Sem r (Maybe MatchError)
+            ok = return Nothing
+            check :: Bool -> Sem r (Maybe MatchError)
+            check b
+              | b = ok
+              | otherwise = err
+            bicheck :: Sem r (Maybe MatchError) -> Sem r (Maybe MatchError) -> Sem r (Maybe MatchError)
+            bicheck = liftA2 (<|>)
+            err :: Sem r (Maybe MatchError)
+            err = return (Just (MatchError a' b'))
+            goHole :: Hole -> Expression -> Sem r (Maybe MatchError)
             goHole h t = do
               r <- queryMetavar' h
               case r of
-                Nothing -> refineFreshMetavar h t $> True
+                Nothing -> refineFreshMetavar h t $> Nothing
                 Just ht -> matchTypes' t ht
-            goIden :: Iden -> Iden -> Sem r Bool
+            goIden :: Iden -> Iden -> Sem r (Maybe MatchError)
             goIden ia ib = case (ia, ib) of
-              (IdenInductive a, IdenInductive b) -> return (a == b)
-              (IdenAxiom a, IdenAxiom b) -> return (a == b)
+              (IdenInductive a, IdenInductive b) -> check (a == b)
+              (IdenAxiom a, IdenAxiom b) -> check (a == b)
               (IdenVar a, IdenVar b) -> do
                 mappedEq <- (== Just b) . HashMap.lookup a <$> ask
-                return (a == b || mappedEq)
-              _ -> return False
-            goApplication :: Application -> Application -> Sem r Bool
-            goApplication (Application f x _) (Application f' x' _) = andM [go f f', go x x']
-            goFunction :: Function -> Function -> Sem r Bool
+                check (a == b || mappedEq)
+              (IdenAxiom {}, _) -> err
+              (_, IdenAxiom {}) -> err
+              (IdenFunction {}, _) -> err
+              (_, IdenFunction {}) -> err
+              (_, IdenVar {}) -> err
+              (IdenVar {}, _) -> err
+              (IdenConstructor {}, _) -> err
+              (_, IdenConstructor {}) -> err
+            goApplication :: Application -> Application -> Sem r (Maybe MatchError)
+            goApplication (Application f x _) (Application f' x' _) = bicheck (go f f') (go x x')
+            goFunction :: Function -> Function -> Sem r (Maybe MatchError)
             goFunction
               (Function (FunctionParameter m1 i1 l1) r1)
               (Function (FunctionParameter m2 i2 l2) r2)
@@ -151,8 +201,8 @@ re = reinterpret $ \case
                         local' = case (m1, m2) of
                           (Just v1, Just v2) -> local (HashMap.insert v1 v2)
                           _ -> id
-                    andM [go l1 l2, local' (go r1 r2)]
-                | otherwise = return False
+                    bicheck (go l1 l2) (local' (go r1 r2))
+                | otherwise = ok
 
 runInference :: Member (Error TypeCheckerError) r => Sem (Inference ': r) Expression -> Sem r Expression
 runInference a = do

test/TypeCheck/Negative.hs

@@ -49,6 +49,13 @@ tests =
       $ \case
         ErrWrongConstructorType {} -> Nothing
         _ -> wrongError,
+    NegTest
+      "Check pattern with hole type"
+      "265"
+      "M.juvix"
+      $ \case
+        ErrWrongConstructorType {} -> Nothing
+        _ -> wrongError,
     NegTest
       "Type vs inferred type mismatch"
       "MicroJuvix"

test/TypeCheck/Positive.hs

@@ -87,6 +87,10 @@ tests =
       "Implicit arguments"
       "MicroJuvix"
       "Implicit.juvix",
+    PosTest
+      "Pattern match a hole type"
+      "265"
+      "M.juvix",
     PosTest
       "Import a builtin multiple times"
       "BuiltinsMultiImport"

tests/negative/265/M.juvix

@@ -0,0 +1,16 @@
+module M;
+
+inductive Bool {
+  false : Bool;
+  true : Bool;
+};
+
+inductive Pair (A : Type) (B : Type) {
+  mkPair : A → B → Pair A B;
+};
+
+f : _ → _;
+f (mkPair false true) ≔ true;
+f true ≔ false;
+
+end;

tests/positive/265/M.juvix

@@ -0,0 +1,16 @@
+module M;
+
+inductive Bool {
+  false : Bool;
+  true : Bool;
+};
+
+inductive Pair (A : Type) (B : Type) {
+  mkPair : A → B → Pair A B;
+};
+
+f : _ → _;
+f (mkPair false true) ≔ true;
+f _ ≔ false;
+
+end;