Type signature sig affects the type of a form properly.

examples/temp.carp

@@ -21,12 +21,22 @@
 
 
 ;; Adding pre-existing functions to interface when it's defined
-(defmodule Foo
+;; (defmodule Foo
-  (defn tripoli [x y z] (Int.= 0 (+ x (+ y z)))))
+;;   (defn tripoli [x y z] (Int.= 0 (+ x (+ y z)))))
 
-;; 'foo' will match this interface that is defined AFTER foo
+;; ;; 'foo' will match this interface that is defined AFTER foo
-(definterface tripoli (λ [Int Int Int] Bool))
+;; (definterface tripoli (λ [Int Int Int] Bool))
 
-;; This should still be added, obviously
+;; ;; This should still be added, obviously
-(defmodule Goo
+;; (defmodule Goo
-  (defn tripoli [x y z] (Int.= 0 (+ x (+ y z)))))
+;;   (defn tripoli [x y z] (Int.= 0 (+ x (+ y z)))))
+
+
+
+;; Type signatures
+
+(sig f (Fn [Int Bool] Float))
+(defn f [] 123)
+
+(sig x Int)
+(def x 2.3)

src/Constraints.hs

@@ -45,6 +45,7 @@ data ConstraintOrder = OrdNo
                      | OrdArrBetween
                      | OrdMultiSym
                      | OrdInterfaceSym
+                     | OrdSignatureAnnotation
                      deriving (Show, Ord, Eq)
 
 data Constraint = Constraint Ty Ty XObj XObj XObj ConstraintOrder deriving Eq

src/Eval.hs

@@ -556,12 +556,6 @@ catcher ctx exception =
             BuildAndRun -> exitWith (ExitFailure returnCode)
             Check -> exitSuccess
 
-existingMeta :: Env -> XObj -> MetaData
-existingMeta globalEnv xobj =
-  case lookupInEnv (getPath xobj) globalEnv of
-    Just (_, Binder meta _) -> meta
-    Nothing -> emptyMeta
-
 -- | Sort different kinds of definitions into the globalEnv or the typeEnv.
 define :: Bool -> Context -> XObj -> IO Context
 define hidden ctx@(Context globalEnv typeEnv _ proj _ _) annXObj =
@@ -582,15 +576,7 @@ define hidden ctx@(Context globalEnv typeEnv _ proj _ _) annXObj =
        XObj (Lst (XObj (DefSumtype _) _ _ : _)) _ _ ->
          return (ctx { contextTypeEnv = TypeEnv (envInsertAt (getTypeEnv typeEnv) (getPath annXObj) (Binder adjustedMeta annXObj)) })
        _ ->
-         do case Map.lookup "sig" (getMeta adjustedMeta) of
+         do when (projectEchoC proj) $
-              Just foundSignature ->
-                do let Just sigTy = xobjToTy foundSignature
-                   unless (areUnifiable (forceTy annXObj) sigTy) $
-                     throw $ EvalException (EvalError ("Definition at " ++ prettyInfoFromXObj annXObj ++ " does not match `sig` annotation " ++
-                              show sigTy ++ ", actual type is `" ++ show (forceTy annXObj) ++ "`.") Nothing fppl)
-              Nothing ->
-                return ()
-            when (projectEchoC proj) $
               putStrLn (toC All (Binder emptyMeta annXObj))
             case previousType of
               Just previousTypeUnwrapped ->
@@ -638,6 +624,19 @@ registerInInterfaceIfNeeded ctx path@(SymPath _ name) definitionSignature =
        Nothing ->
          return ctx
 
+getSigFromDefnOrDef :: Env -> XObj -> StateT Context IO (Either EvalError (Maybe (Ty, XObj)))
+getSigFromDefnOrDef globalEnv xobj =
+  let metaData = existingMeta globalEnv xobj
+  in  case Map.lookup "sig" (getMeta metaData) of
+        Just foundSignature ->
+          case xobjToTy foundSignature of
+            Just t -> let sigToken = XObj (Sym (SymPath [] "sig") Symbol) Nothing Nothing
+                          nameToken = XObj (Sym (SymPath [] (getName xobj)) Symbol) Nothing Nothing
+                          recreatedSigForm = XObj (Lst [sigToken, nameToken, foundSignature]) Nothing (Just MacroTy)
+                      in return (Right (Just (t, recreatedSigForm)))
+            Nothing -> error ("TODO: Return error here, failed to convert " ++ pretty foundSignature ++ " to a type.")
+        Nothing -> return (Right Nothing)
+
 annotateWithinContext :: Bool -> XObj -> StateT Context IO (Either EvalError (XObj, [XObj]))
 annotateWithinContext qualifyDefn xobj =
   do ctx <- get
@@ -646,23 +645,27 @@ annotateWithinContext qualifyDefn xobj =
          globalEnv = contextGlobalEnv ctx
          typeEnv = contextTypeEnv ctx
          innerEnv = getEnv globalEnv pathStrings
+     sig <- getSigFromDefnOrDef globalEnv xobj
      expansionResult <- expandAll eval globalEnv xobj
      ctxAfterExpansion <- get
-     case expansionResult of
+     case sig of
-       Left err -> return (makeEvalError ctx Nothing (show err) Nothing)
+       Left err -> return (Left err)
-       Right expanded ->
+       Right okSig ->
-         let xobjFullPath = if qualifyDefn then setFullyQualifiedDefn expanded (SymPath pathStrings (getName xobj)) else expanded
+         case expansionResult of
-             xobjFullSymbols = setFullyQualifiedSymbols typeEnv globalEnv innerEnv xobjFullPath
+           Left err -> return (makeEvalError ctx Nothing (show err) Nothing)
-         in case annotate typeEnv globalEnv xobjFullSymbols of
+           Right expanded ->
-              Left err ->
+             let xobjFullPath = if qualifyDefn then setFullyQualifiedDefn expanded (SymPath pathStrings (getName xobj)) else expanded
-                case contextExecMode ctx of
+                 xobjFullSymbols = setFullyQualifiedSymbols typeEnv globalEnv innerEnv xobjFullPath
-                  Check ->
+             in case annotate typeEnv globalEnv xobjFullSymbols okSig of
-                    let fppl = projectFilePathPrintLength (contextProj ctx)
+                  Left err ->
-                    in  return (Left (EvalError (joinWith "\n" (machineReadableErrorStrings fppl err)) Nothing fppl))
+                    case contextExecMode ctx of
-                  _ ->
+                      Check ->
-                    return (Left (EvalError (show err) Nothing fppl))
+                        let fppl = projectFilePathPrintLength (contextProj ctx)
-              Right ok ->
+                        in  return (Left (EvalError (joinWith "\n" (machineReadableErrorStrings fppl err)) Nothing fppl))
-                return (Right ok)
+                      _ ->
+                        return (Left (EvalError (show err) Nothing fppl))
+                  Right ok ->
+                    return (Right ok)
 
 -- | SPECIAL FORM COMMANDS (needs to get access to unevaluated arguments, which makes them "special forms" in Lisp lingo)
 
@@ -1284,7 +1287,7 @@ commandC [xobj] =
      case result of
        Left err -> return (Left (EvalError (show err) (info xobj)))
        Right expanded ->
-         case annotate typeEnv globalEnv (setFullyQualifiedSymbols typeEnv globalEnv globalEnv expanded) of
+         case annotate typeEnv globalEnv (setFullyQualifiedSymbols typeEnv globalEnv globalEnv expanded) Nothing of
            Left err -> return (Left (EvalError (show err) (info xobj)))
            Right (annXObj, annDeps) ->
              do let cXObj = printC annXObj

src/GenerateConstraints.hs

@@ -6,6 +6,7 @@ import Control.Monad.State
 import Data.Maybe (mapMaybe, fromMaybe)
 import Data.Set as Set
 import Data.List as List
+import Data.Map as Map (lookup)
 import Debug.Trace (trace)
 
 import Types
@@ -16,8 +17,8 @@ import TypeError
 import Lookup
 
 -- | Will create a list of type constraints for a form.
-genConstraints :: TypeEnv -> XObj -> Either TypeError [Constraint]
+genConstraints :: Env -> XObj -> Maybe (Ty, XObj) -> Either TypeError [Constraint]
-genConstraints typeEnv root = fmap sort (gen root)
+genConstraints globalEnv root rootSig = fmap sort (gen root)
   where genF xobj args body captures =
          do insideBodyConstraints <- gen body
             xobjType <- toEither (ty xobj) (DefnMissingType xobj)
@@ -25,6 +26,10 @@ genConstraints typeEnv root = fmap sort (gen root)
             let (FuncTy argTys retTy lifetimeTy) = xobjType
                 bodyConstr = Constraint retTy bodyType xobj body xobj OrdDefnBody
                 argConstrs = zipWith3 (\a b aObj -> Constraint a b aObj xobj xobj OrdArg) (List.map forceTy args) argTys args
+                -- The constraint generated by type signatures, like (sig foo (Fn ...)):
+                sigConstr = case rootSig of
+                              Just (rootSigTy, rootSigXObj) -> [Constraint rootSigTy xobjType rootSigXObj xobj xobj OrdSignatureAnnotation]
+                              Nothing -> []
                 captureList :: [XObj]
                 captureList = Set.toList captures
                 capturesConstrs = mapMaybe id
@@ -38,7 +43,7 @@ genConstraints typeEnv root = fmap sort (gen root)
                                                     Nothing)
                                       (List.map forceTy captureList)
                                       captureList)
-            return (bodyConstr : argConstrs ++ insideBodyConstraints ++ capturesConstrs)
+            return (bodyConstr : argConstrs ++ insideBodyConstraints ++ capturesConstrs ++ sigConstr)
         gen xobj =
           case obj xobj of
             Lst lst -> case lst of
@@ -56,7 +61,10 @@ genConstraints typeEnv root = fmap sort (gen root)
                                 xobjType <- toEither (ty xobj) (DefMissingType xobj)
                                 exprType <- toEither (ty expr) (ExpressionMissingType xobj)
                                 let defConstraint = Constraint xobjType exprType xobj expr xobj OrdDefExpr
-                                return (defConstraint : insideExprConstraints)
+                                    sigConstr = case rootSig of
+                                                  Just (rootSigTy, rootSigXObj) -> [Constraint rootSigTy xobjType rootSigXObj xobj xobj OrdSignatureAnnotation]
+                                                  Nothing -> []
+                                return (defConstraint : insideExprConstraints ++ sigConstr)
 
                            -- Let
                            [XObj Let _ _, XObj (Arr bindings) _ _, body] ->

src/Infer.hs

@@ -29,30 +29,30 @@ import Concretize
 -- | Returns a list of all the bindings that need to be added for the new form to work.
 -- | The concretization of MultiSym:s (= ambiguous use of symbols, resolved by type usage)
 -- | makes it possible to solve more types so let's do it several times.
-annotate :: TypeEnv -> Env -> XObj -> Either TypeError (XObj, [XObj])
+annotate :: TypeEnv -> Env -> XObj -> Maybe (Ty, XObj) -> Either TypeError (XObj, [XObj])
-annotate typeEnv globalEnv xobj =
+annotate typeEnv globalEnv xobj rootSig =
   do initiated <- initialTypes typeEnv globalEnv xobj
-     (annotated, dependencies) <- annotateUntilDone typeEnv globalEnv initiated [] 100
+     (annotated, dependencies) <- annotateUntilDone typeEnv globalEnv initiated rootSig [] 100
      (final, deleteDeps) <- manageMemory typeEnv globalEnv annotated
      finalWithNiceTypes <- beautifyTypeVariables final
      return (finalWithNiceTypes, dependencies ++ deleteDeps)
 
 -- | Call the 'annotateOne' function until nothing changes
-annotateUntilDone :: TypeEnv -> Env -> XObj -> [XObj] -> Int -> Either TypeError (XObj, [XObj])
+annotateUntilDone :: TypeEnv -> Env -> XObj -> Maybe (Ty, XObj) -> [XObj] -> Int -> Either TypeError (XObj, [XObj])
-annotateUntilDone typeEnv globalEnv xobj deps limiter =
+annotateUntilDone typeEnv globalEnv xobj rootSig deps limiter =
   if limiter <= 0
   then Left (TooManyAnnotateCalls xobj)
-  else do (xobj', deps') <- annotateOne typeEnv globalEnv xobj True
+  else do (xobj', deps') <- annotateOne typeEnv globalEnv xobj rootSig True
           let newDeps = deps ++ deps'
           if xobj == xobj' -- Is it the same?
             then return (xobj', newDeps)
-            else annotateUntilDone typeEnv globalEnv xobj' newDeps (limiter - 1)
+            else annotateUntilDone typeEnv globalEnv xobj' rootSig newDeps (limiter - 1)
 
 -- | Performs ONE step of annotation. The 'annotate' function will call this function several times.
 -- | TODO: Remove the allowAmbiguity flag?
-annotateOne :: TypeEnv -> Env -> XObj -> Bool -> Either TypeError (XObj, [XObj])
+annotateOne :: TypeEnv -> Env -> XObj -> Maybe (Ty, XObj) -> Bool -> Either TypeError (XObj, [XObj])
-annotateOne typeEnv env xobj allowAmbiguity = do
+annotateOne typeEnv env xobj rootSig allowAmbiguity = do
-  constraints <- genConstraints typeEnv xobj
+  constraints <- genConstraints env xobj rootSig
   mappings <- solveConstraintsAndConvertErrorIfNeeded constraints -- (trace ("Constraints for '" ++ getName xobj ++ "':\n" ++ joinWith "\n" (map show constraints)) constraints)
   typed <- assignTypes mappings xobj -- (trace ("Mappings for '" ++ getName xobj ++ ": " ++ show mappings) mappings) xobj
   concretizeXObj allowAmbiguity typeEnv env [] typed

src/Lookup.hs

@@ -231,3 +231,9 @@ bindingNames = concatMap select . envBindings
   where select :: Binder -> [String]
         select (Binder _ (XObj (Mod i) _ _)) = bindingNames i
         select (Binder _ obj) = [getName obj]
+
+existingMeta :: Env -> XObj -> MetaData
+existingMeta globalEnv xobj =
+  case lookupInEnv (getPath xobj) globalEnv of
+    Just (_, Binder meta _) -> meta
+    Nothing -> emptyMeta

src/Obj.hs

@@ -378,6 +378,7 @@ metaIsTrue metaData key =
     _ -> False
 
 
+
 -- | Wraps and holds an XObj in an environment.
 data Binder = Binder { binderMeta :: MetaData, binderXObj :: XObj } deriving Eq