Merge pull request #2094 from GaloisInc/2071-dholland-positioning

Rework the position tracking for types.

intTests/test_type_errors/err001.log.good

@@ -1,6 +1,8 @@
  Loading file "err001.saw"
  err001.saw:1:23-1:24: Type mismatch.
     Mismatch of type constructors. Expected: String but got Int
+    err001.saw:1:14-1:20: The type String arises from this type annotation
+    err001.saw:1:23-1:24: The type Int arises from the type of this term
 
     Expected: String
     Found:    Int

src/SAWScript/AST.hs

@@ -208,18 +208,37 @@ data Context
   | CrucibleSetup
   deriving (Eq,Show)
 
+-- The position information in a type should be thought of as its
+-- provenance; for a type annotation in the input it'll be a concrete
+-- file position. For types we infer, we want the position to record
+-- not just where but also how the inference happened, so that when we
+-- report this to the user they can see what's going on. (For example,
+-- if we infer that a type must be a function because it's applied to
+-- an argument, we record that it's inferred from context and the
+-- position of the context is the position of the term that was
+-- applied.) When the type flows around during type inference it
+-- carries the position info with it.
+--
+-- Note that for a non-primitive type the various layers of the type
+-- may have totally different provenance. (E.g. we might have List Int
+-- where List was inferred from a term "[x]" somewhere but Int came
+-- from an explicit annotation somewhere completely different.) So
+-- printing this information usefully requires some thought. As of
+-- this writing most of that thought hasn't been put in yet and we
+-- just stuff the inference info into the Show instance output. See
+-- notes in Position.hs.
 data Type
-  = TyCon TyCon [Type]
-  | TyRecord (Map Name Type)
-  | TyVar Name
-  | TyUnifyVar TypeIndex       -- ^ For internal typechecker use only
-  | TySkolemVar Name TypeIndex -- ^ For internal typechecker use only
-  | LType Pos Type
+  = TyCon Pos TyCon [Type]
+  | TyRecord Pos (Map Name Type)
+  | TyVar Pos Name
+  | TyUnifyVar Pos TypeIndex       -- ^ For internal typechecker use only
   deriving Show
 
 instance Positioned Type where
-  getPos (LType pos _) = pos
-  getPos _ = Unknown
+  getPos (TyCon pos _ _) = pos
+  getPos (TyRecord pos _) = pos
+  getPos (TyVar pos _) = pos
+  getPos (TyUnifyVar pos _) = pos
 
 type TypeIndex = Integer
 
@@ -241,7 +260,7 @@ data TyCon
   | ContextCon Context
   deriving (Eq, Show)
 
-data Schema = Forall [Name] Type
+data Schema = Forall [(Pos, Name)] Type
   deriving Show
 
 -- }}}
@@ -382,10 +401,11 @@ class PrettyPrint p where
 instance PrettyPrint Schema where
   pretty _ (Forall ns t) = case ns of
     [] -> pretty 0 t
-    _  -> PP.braces (commaSepAll $ map PP.pretty ns) PP.<+> pretty 0 t
+    _  -> PP.braces (commaSepAll $ map PP.pretty ns') PP.<+> pretty 0 t
+          where ns' = map (\(_pos, n) -> n) ns
 
 instance PrettyPrint Type where
-  pretty par t@(TyCon tc ts) = case (tc,ts) of
+  pretty par t@(TyCon _ tc ts) = case (tc,ts) of
     (_,[])                 -> pretty par tc
     (TupleCon _,_)         -> PP.parens $ commaSepAll $ map (pretty 0) ts
     (ArrayCon,[typ])       -> PP.brackets (pretty 0 typ)
@@ -394,15 +414,13 @@ instance PrettyPrint Type where
     (BlockCon,[cxt,typ])   -> (if par > 1 then PP.parens else id) $
                                 pretty 1 cxt PP.<+> pretty 2 typ
     _ -> error $ "malformed TyCon: " ++ show t
-  pretty _par (TyRecord fs) =
+  pretty _par (TyRecord _ fs) =
       PP.braces
     $ commaSepAll
     $ map (\(n,t) -> PP.pretty n `prettyTypeSig` pretty 0 t)
     $ Map.toList fs
-  pretty _par (TyUnifyVar i)    = "t." PP.<> PP.pretty i
-  pretty _par (TySkolemVar n i) = PP.pretty n PP.<> PP.pretty i
-  pretty _par (TyVar n)         = PP.pretty n
-  pretty par (LType _ t)        = pretty par t
+  pretty _par (TyUnifyVar _ i)    = "t." PP.<> PP.pretty i
+  pretty _par (TyVar _ n)         = PP.pretty n
 
 instance PrettyPrint TyCon where
   pretty par tc = case tc of
@@ -455,59 +473,59 @@ commaSepAll ds = case ds of
 tMono :: Type -> Schema
 tMono = Forall []
 
-tForall :: [Name] -> Schema -> Schema
+tForall :: [(Pos, Name)] -> Schema -> Schema
 tForall xs (Forall ys t) = Forall (xs ++ ys) t
 
-tTuple :: [Type] -> Type
-tTuple ts = TyCon (TupleCon $ fromIntegral $ length ts) ts
+tTuple :: Pos -> [Type] -> Type
+tTuple pos ts = TyCon pos (TupleCon $ fromIntegral $ length ts) ts
 
-tRecord :: [(Name, Type)] -> Type
-tRecord fields = TyRecord (Map.fromList fields)
+tRecord :: Pos -> [(Name, Type)] -> Type
+tRecord pos fields = TyRecord pos (Map.fromList fields)
 
-tArray :: Type -> Type
-tArray t = TyCon ArrayCon [t]
+tArray :: Pos -> Type -> Type
+tArray pos t = TyCon pos ArrayCon [t]
 
-tFun :: Type -> Type -> Type
-tFun f v = TyCon FunCon [f,v]
+tFun :: Pos -> Type -> Type -> Type
+tFun pos f v = TyCon pos FunCon [f,v]
 
-tString :: Type
-tString = TyCon StringCon []
+tString :: Pos -> Type
+tString pos = TyCon pos StringCon []
 
-tTerm :: Type
-tTerm = TyCon TermCon []
+tTerm :: Pos -> Type
+tTerm pos = TyCon pos TermCon []
 
-tType :: Type
-tType = TyCon TypeCon []
+tType :: Pos -> Type
+tType pos = TyCon pos TypeCon []
 
-tBool :: Type
-tBool = TyCon BoolCon []
+tBool :: Pos -> Type
+tBool pos = TyCon pos BoolCon []
 
-tAIG :: Type
-tAIG = TyCon AIGCon []
+tAIG :: Pos -> Type
+tAIG pos = TyCon pos AIGCon []
 
-tCFG :: Type
-tCFG = TyCon CFGCon []
+tCFG :: Pos -> Type
+tCFG pos = TyCon pos CFGCon []
 
-tInt :: Type
-tInt = TyCon IntCon []
+tInt :: Pos -> Type
+tInt pos = TyCon pos IntCon []
 
-tJVMSpec :: Type
-tJVMSpec = TyCon JVMSpecCon []
+tJVMSpec :: Pos -> Type
+tJVMSpec pos = TyCon pos JVMSpecCon []
 
-tLLVMSpec :: Type
-tLLVMSpec = TyCon LLVMSpecCon []
+tLLVMSpec :: Pos -> Type
+tLLVMSpec pos = TyCon pos LLVMSpecCon []
 
-tMIRSpec :: Type
-tMIRSpec = TyCon MIRSpecCon []
+tMIRSpec :: Pos -> Type
+tMIRSpec pos = TyCon pos MIRSpecCon []
 
-tBlock :: Type -> Type -> Type
-tBlock c t = TyCon BlockCon [c,t]
+tBlock :: Pos -> Type -> Type -> Type
+tBlock pos c t = TyCon pos BlockCon [c,t]
 
-tContext :: Context -> Type
-tContext c = TyCon (ContextCon c) []
+tContext :: Pos -> Context -> Type
+tContext pos c = TyCon pos (ContextCon c) []
 
-tVar :: Name -> Type
-tVar n = TyVar n
+tVar :: Pos -> Name -> Type
+tVar pos n = TyVar pos n
 
 -- }}}
 
@@ -523,7 +541,7 @@ isContext ::
     -> Type             -- ^ The type 'ty' to inspect
     -> Bool
 isContext c ty = case ty of
-  TyCon (ContextCon c') [] | c' == c -> True
+  TyCon _pos (ContextCon c') [] | c' == c -> True
   _ -> False
 
 -- }}}

src/SAWScript/Interpreter.hs

@@ -131,7 +131,7 @@ bindPatternLocal pat ms v env =
         VTuple vs -> foldr ($) env (zipWith3 bindPatternLocal ps mss vs)
           where mss = case ms of
                   Nothing -> repeat Nothing
-                  Just (SS.Forall ks (SS.TyCon (SS.TupleCon _) ts))
+                  Just (SS.Forall ks (SS.TyCon _ (SS.TupleCon _) ts))
                     -> [ Just (SS.Forall ks t) | t <- ts ]
                   Just t -> error ("bindPatternLocal: expected tuple type " ++ show t)
         _ -> error "bindPatternLocal: expected tuple value"
@@ -148,7 +148,7 @@ bindPatternEnv pat ms v env =
         VTuple vs -> foldr (=<<) (pure env) (zipWith3 bindPatternEnv ps mss vs)
           where mss = case ms of
                   Nothing -> repeat Nothing
-                  Just (SS.Forall ks (SS.TyCon (SS.TupleCon _) ts))
+                  Just (SS.Forall ks (SS.TyCon _ (SS.TupleCon _) ts))
                     -> [ Just (SS.Forall ks t) | t <- ts ]
                   Just t -> error ("bindPatternEnv: expected tuple type " ++ show t)
         _ -> error "bindPatternEnv: expected tuple value"
@@ -211,9 +211,10 @@ locToInput l = CEnv.InputText { CEnv.inpText = getVal l
                               , CEnv.inpCol  = col + 2 -- for dropped }}
                               }
   where
-  (file,ln,col) =
-    case locatedPos l of
+  (file, ln, col) = extract $ locatedPos l
+  extract pos = case pos of
       SS.Range f sl sc _ _ -> (f,sl, sc)
+      SS.PosInferred _ pos' -> extract pos'
       SS.PosInternal s -> (s,1,1)
       SS.PosREPL       -> ("<interactive>", 1, 1)
       SS.Unknown       -> ("Unknown", 1, 1)
@@ -299,10 +300,16 @@ processStmtBind printBinds pat _mc expr = do -- mx mt
         SS.PVar _pos x t -> (x, t)
         SS.PTuple pos _pats -> (it pos, Nothing)
   ctx <- getMonadContext
-  let tyctx = SS.tContext ctx
+  -- XXX SS.PosREPL probably is not what we want
+  -- but the position we want for the block type isn't the position of
+  -- the pattern (perhaps we want the position of the "do" that makes
+  -- this a block context? but there isn't necessarily one in the
+  -- repl)
+  let pos = SS.PosREPL
+  let tyctx = SS.tContext pos ctx
   let expr' = case mt of
                 Nothing -> expr
-                Just t -> SS.TSig (SS.maxSpan' expr t) expr (SS.tBlock tyctx t)
+                Just t -> SS.TSig (SS.maxSpan' expr t) expr (SS.tBlock pos tyctx t)
   let decl = SS.Decl (SS.maxSpan' pat expr') pat Nothing expr'
   rw <- liftTopLevel getMergedEnv
   let opts = rwPPOpts rw
@@ -317,7 +324,7 @@ processStmtBind printBinds pat _mc expr = do -- mx mt
     case schema of
       SS.Forall [] t ->
         case t of
-          SS.TyCon SS.BlockCon [c, t'] | SS.isContext ctx c -> do
+          SS.TyCon _ SS.BlockCon [c, t'] | SS.isContext ctx c -> do
             result <- actionFromValue val
             return (result, t')
           _ -> return (val, t)
@@ -335,7 +342,7 @@ processStmtBind printBinds pat _mc expr = do -- mx mt
 
   -- Print function type if result was a function
   case ty of
-    SS.TyCon SS.FunCon _ ->
+    SS.TyCon _ SS.FunCon _ ->
       liftTopLevel $ printOutLnTop Info $ getVal lname ++ " : " ++ SS.pShow ty
     _ -> return ()