Fix module-related scoping issues in errors (#218)

* Qualify names when leaving a module

And, indeed, unqualify names when leaving a module. In practice, this
means that the entire TC scope consists of types that are writable, as
printed, in the scope they are referring to.

* Keep names qualified when resolving

src/Syntax/Builtin.hs

@@ -101,9 +101,9 @@ tyArrow      = TyCon tyArrowName
 tyList       = TyCon tyListName
 tyConstraint = TyCon tyConstraintName
 tyRef        = TyCon tyRefName
-tyKStr       = TyCon tyKStrName
-tyKInt       = TyCon tyKIntName
-tyRowCons    = TyCon rowConsName
+tyKStr       = TyCon (TgInternal "Amc" <> tyKStrName)
+tyKInt       = TyCon (TgInternal "Amc" <> tyKIntName)
+tyRowCons    = TyCon (TgInternal "Amc" <> rowConsName)
 tyEq         = TyCon tyEqName
 
 forceName, lAZYName :: Var Typed

src/Syntax/Resolve.hs

@@ -599,7 +599,12 @@ lookupIn g nonRec v k = go v where
 lookupSlot :: MonadResolve m
            => Var Parsed -> Slot
            -> m (Var Resolved)
-lookupSlot _ (SVar x) = pure x
+lookupSlot v (SVar x) = pure $
+  let toName (Name x) = x
+      toName (InModule t x) = t <> T.singleton '.' <> toName x
+   in case x of
+     TgInternal n -> TgInternal n
+     TgName _ id -> TgName (toName v) id
 lookupSlot v (SAmbiguous vs) = confesses (Ambiguous v vs)
 
 -- | Lookup a value/expression variable.

src/Syntax/Types.hs

@@ -3,7 +3,7 @@
   , TypeFamilies, TemplateHaskell, FunctionalDependencies, RankNTypes #-}
 module Syntax.Types
   ( Telescope, one, foldTele, foldTeleM, teleFromList, mapTele, traverseTele, teleToList
-  , Scope(..), namesInScope, inScope, scopeToList
+  , Scope(..), namesInScope, inScope, scopeToList, mapScope
   , Env, freeInEnv, difference, envOf, scopeFromList, toMap
   , names, typeVars, constructors, types, letBound, classes, modules
   , classDecs, tySyms, declaredHere
@@ -203,6 +203,9 @@ scopeToList (Scope m) = Map.toList m
 inScope :: Ord (Var p) => Var p -> Scope p f -> Bool
 inScope v (Scope m) = v `Map.member` m
 
+mapScope :: (Var p -> Var p) -> (f -> f) -> Scope p f -> Scope p f
+mapScope k k' (Scope m) = Scope (k' <$> Map.mapKeysMonotonic k m)
+
 focus :: Telescope t -> Scope Resolved (Type t) -> Scope Resolved (Type t)
 focus m s = Scope (getScope s <> getTele m)
 

src/Syntax/Verify.hs

@@ -1,6 +1,6 @@
 {-# LANGUAGE ConstraintKinds, FlexibleContexts, FlexibleInstances,
    UndecidableInstances, MultiParamTypeClasses, OverloadedStrings,
-   ScopedTypeVariables, TupleSections #-}
+   ScopedTypeVariables, TupleSections, GADTs #-}
 module Syntax.Verify
   ( VerifyError(..)
   , BindingSite(..)
@@ -9,6 +9,7 @@ module Syntax.Verify
   ) where
 
 import qualified Data.Sequence as Seq
+import qualified Data.Text as T
 import qualified Data.Set as Set
 import Data.Foldable
 import Data.Reason
@@ -26,6 +27,7 @@ import Syntax.Verify.Pattern
 import Syntax.Verify.Error
 
 import Syntax.Builtin (tyLazy, forceName, tyRefName)
+import Syntax.Transform
 import Syntax.Types
 import Syntax.Let
 import Syntax
@@ -81,7 +83,22 @@ verifyProgram = traverse_ verifyStmt where
   verifyStmt TypeDecl{} = pure ()
   verifyStmt DeriveInstance{} = pure ()
   verifyStmt TypeFunDecl{} = pure ()
-  verifyStmt (Module _ _ m) = verifyModule m
+
+  -- Here we do the opposite of TC: Since we're working with the final
+  -- 'Env' (where everything is fully qualified), when entering a module
+  -- definition, remove the prefix.
+  verifyStmt (Module _ nm m) = do
+    let prefix = case nm of
+          TgName n _ -> n <> T.singleton '.'
+          TgInternal v -> v <> T.singleton '.'
+
+    let go (VerifyScope env m) =
+          flip VerifyScope m $
+            env & names %~ mapScope id (unqualifyWrt prefix)
+                & types %~ fmap (Set.mapMonotonic (unqualifyVarWrt prefix))
+
+    local go $ verifyModule m
+
   verifyStmt (Open m) = verifyModule m
   verifyStmt (Include m) = verifyModule m
 
@@ -329,3 +346,14 @@ verifyMatch rep m ty bs = do
     (Seq.Empty, [a]) | ok -> rep a
     (Seq.Empty, _) -> pure ()
     (_, _) -> tell . pure . MissingPattern m . map snd . toList $ unc
+
+unqualifyWrt :: (Var p ~ Var Resolved) => T.Text -> Type p -> Type p
+unqualifyWrt n = transformType go where
+  go (TyCon v) = TyCon (unqualifyVarWrt n v)
+  go t = t
+
+unqualifyVarWrt :: T.Text -> Var Resolved -> Var Resolved
+unqualifyVarWrt n (TgName v id)
+  | n `T.isPrefixOf` v = TgName (T.drop (T.length n) v) id
+  | otherwise = TgName v id
+unqualifyVarWrt _ n = n

src/Types/Infer.hs

@@ -312,7 +312,7 @@ infer (Begin xs a) = do
 
 infer (OpenIn mod expr a) = do
   (mod', exEnv, (modImplicits, modTysym)) <- inferMod mod
-  local (exEnv . (classes %~ (<>modImplicits)) . (tySyms %~ (<>modTysym))) $ do
+  local (unqualify mod . exEnv Nothing . (classes %~ (<>modImplicits)) . (tySyms %~ (<>modTysym))) $ do
     (expr', ty) <- infer expr
     pure (ExprWrapper (TypeAsc ty) (OpenIn mod' (ExprWrapper (TypeAsc ty) expr' (a, ty)) (a, ty)) (a, ty), ty)
 
@@ -492,37 +492,52 @@ inferProg (DeriveInstance tau ann:prg) = do
 
 inferProg (Open mod:prg) = do
   (mod', exEnv, (modImplicits, modTysym)) <- inferMod mod
-  local (exEnv. (classes %~ (<>modImplicits)) . (tySyms %~ (<>modTysym))) $
+
+  local (unqualify mod . exEnv Nothing . (classes %~ (<>modImplicits)) . (tySyms %~ (<>modTysym))) $
     consFst (Open mod') $ inferProg prg
 
 inferProg (Include mod:prg) = do
   (mod', exEnv, (modImplicits, modTysym)) <- inferMod mod
-  local (exEnv. (classes %~ (<>modImplicits)) . (tySyms %~ (<>modTysym))) $
+
+  local (unqualify mod . exEnv Nothing . (classes %~ (<>modImplicits)) . (tySyms %~ (<>modTysym))) $
     consFst (Include mod') $ inferProg prg
 
 inferProg (Module am name mod:prg) = do
   (mod', exEnv, modInfo) <- local (declaredHere .~ mempty) $ inferMod mod
-  local (exEnv . (modules %~ Map.insert name modInfo)) $
+  local (exEnv (Just name) . (modules %~ Map.insert name modInfo)) $
     consFst (Module am name mod') $
     inferProg prg
 
 inferProg [] = asks ([],)
 
 inferMod :: MonadInfer Typed m => ModuleTerm Desugared
-         -> m (ModuleTerm Typed, Env -> Env, (ImplicitScope ClassInfo Typed, TySyms))
+         -> m (ModuleTerm Typed, Maybe (Var Resolved) -> Env -> Env, (ImplicitScope ClassInfo Typed, TySyms))
 inferMod (ModStruct bod a) = do
   (bod', env) <- inferProg bod
   -- So this behaviour is somewhat incorrect, as we'll exposed any type
   -- functions/implicits that we open in our signature. But it'll do for now.
+  let append x p = maybe p (<> p) x
+      qualifyWrt prefix scope =
+        let go (TyCon n) = 
+              if n `inScope` scope
+                 then TyCon (append prefix n)
+                 else TyCon n
+            go x = x
+         in transformType go
+
   pure (ModStruct bod' (a, undefined)
-       , (names %~ (<> (env ^. names)))
-       . (types %~ (<> (env ^. types)))
-       . (classDecs %~ (<> (env ^. classDecs)))
-       . (modules %~ (<> (env ^. modules)))
+       , \prefix ->
+           (names %~ (<> mapScope (append prefix) (qualifyWrt prefix (env ^. names)) (env ^. names)))
+         . (types %~ (<> (Set.mapMonotonic (append prefix)
+                            <$> Map.mapKeysMonotonic (append prefix) (env ^. types))))
+         . (classDecs %~ (<> (env ^. classDecs)))
+         . (modules %~ (<> Map.mapKeysMonotonic (append prefix) (env ^. modules)))
        , (env ^. classes, env ^. tySyms))
+
 inferMod (ModRef name a) = do
   mod <- view (modules . at name) >>= maybe (confesses (NotInScope name)) pure
-  pure (ModRef name (a, undefined), id, mod)
+  pure (ModRef name (a, undefined), const id, mod)
+
 inferMod ModLoad{} = error "Impossible"
 
 buildList :: Ann Resolved -> Type Typed -> [Expr Typed] -> Expr Typed
@@ -631,3 +646,25 @@ isReflexiveCo (ForallCo _ _ a b) = isReflexiveCo a && isReflexiveCo b
 isReflexiveCo P1{} = False
 isReflexiveCo P2{} = False
 isReflexiveCo InstCo{} = False
+
+unqualifyWrt :: (Var p ~ Var Resolved) => T.Text -> Type p -> Type p
+unqualifyWrt n = transformType go where
+  go (TyCon v) = TyCon (unqualifyVarWrt n v)
+  go t = t
+
+unqualifyVarWrt :: T.Text -> Var Resolved -> Var Resolved
+unqualifyVarWrt n (TgName v id)
+  | n `T.isPrefixOf` v = TgName (T.drop (T.length n) v) id
+  | otherwise = TgName v id
+unqualifyVarWrt _ n = n
+
+unqualify :: (Var p ~ Var Resolved) => ModuleTerm p -> Env -> Env
+unqualify (ModRef v _) =
+ let prefix =
+       case v of
+         TgName v _ -> v <> T.singleton '.'
+         TgInternal v -> v <> T.singleton '.'
+  in (names %~ mapScope id (unqualifyWrt prefix))
+   . (types %~ fmap (Set.mapMonotonic (unqualifyVarWrt prefix)))
+
+unqualify _ = id

tests/resolve/pass_include.out

@@ -6,4 +6,4 @@ module Y#2 = begin
   include X#0
 end
 foreign val +#4 : int -> int -> int = "function(x, y) return x + y end"
-let _ = (x#1 +#4 y#3)
+let _ = (Y.x#1 +#4 Y.y#3)

tests/resolve/pass_modules.out

@@ -4,7 +4,7 @@ module X#0 = begin
   end
 end
 module Z#3 = Y#1
-let a#4 = x#2
+let a#4 = Z.x#2
 open X#0
-let b#5 = x#2
-let z#6 = X#0.({ a = x#2 })
+let b#5 = Y.x#2
+let z#6 = X#0.({ a = Y.x#2 })

tests/types/class/assoc-eta.out

@@ -1,5 +1,5 @@
 has_sing : Req{'k : type}. constraint
 sing_t : Req{'k : type}. 'k -> type
 sint : int -> type
-SInt : Spec{'i : int}. known_int 'i => sint 'i
+SInt : Spec{'i : int}. Amc.known_int 'i => sint 'i
 sing : sing_t int 123

tests/types/class/row-cons-fail.out

@@ -1,5 +1,5 @@
 row-cons-fail.ml[1:9 ..1:39]: error (E2018)
-  No instance for row_cons 'record "y" 'type { x : int } arising in this expression
+  No instance for Amc.row_cons 'record "y" 'type { x : int } arising in this expression
   │ 
 1 │ let x = Amc.restrict_row @"y" { x = 1 }
   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

tests/types/letopen.out

@@ -1,2 +1,2 @@
-foo : Req{'a : type}. constraint
-foo_it : Spec{'a : type}. foo 'a => 'a -> unit
+Foo.foo : Req{'a : type}. constraint
+Foo.foo_it : Spec{'a : type}. Foo.foo 'a => 'a -> Foo.unit

tests/types/scope.ml

@@ -0,0 +1,19 @@
+external val (+) : int -> int -> int =
+  "function(x, y) return x + y end"
+
+module X = begin
+  type t = T
+  let x = T
+end
+
+let _ =
+  let _ = X.x + 1
+  (* local opens unqualify *)
+  let _ =
+    let open X
+    x + 1
+  let _ = X.( x + 1 )
+
+  (* make sure that the unqualified scope doesn't leak *)
+  let _ = X.x + 1
+  ()

tests/types/scope.out

@@ -0,0 +1,24 @@
+scope.ml[10:11 ..10:13]: error (E2001)
+   │ 
+10 │   let _ = X.x + 1
+   │           ^^^
+  Couldn't match actual type X.t
+    with the type expected by the context, int
+scope.ml[14:5 ..14:5]: error (E2001)
+   │ 
+14 │     x + 1
+   │     ^
+  Couldn't match actual type t
+    with the type expected by the context, int
+scope.ml[15:15 ..15:15]: error (E2001)
+   │ 
+15 │   let _ = X.( x + 1 )
+   │               ^
+  Couldn't match actual type t
+    with the type expected by the context, int
+scope.ml[18:11 ..18:13]: error (E2001)
+   │ 
+18 │   let _ = X.x + 1
+   │           ^^^
+  Couldn't match actual type X.t
+    with the type expected by the context, int