on master help sign in
Added instantiation
commit81d54f2bc6dd68c2342002088b4568c2fef5129e authoriko <ilyakooo0@gmail.com> dateMon 8 Mar 2021, 21:56 (6 years ago) parent06a4889
4 files changed+29
src/Tix/Typechecker.hs+26 test/golden/importless/nuget.txt+1 test/golden/importless/require_exceptions.txt+1 test/golden/importless/xsa-patches.txt+1
src/Tix/Typechecker.hs+26
@@ -294,6 +294,7 @@ type VariableMap = Map VarName NType
294294(~~) :: Member (Writer Constraint) r => NType -> NType -> Eff r ()
295295lhs ~~ rhs = tell $ lhs :~ rhs
296296
297+-- TODO: shadowed bindings are not properly restored.
297298withBindings ::
298299 (Member (State VariableMap) effs) =>
299300 VariableMap ->
@@ -305,6 +306,30 @@ withBindings bindings m = do
305306 modify @VariableMap (`M.difference` bindings)
306307 return a
307308
309+instantiate ::
310+ forall effs.
311+ Members '[Fresh, Reader SrcSpan, Writer (TypeVariable, SrcSpan)] effs =>
312+ NType ->
313+ Eff effs NType
314+instantiate = evalState M.empty . instantiate'
315+ where
316+ instantiate' :: forall. NType -> Eff (State (Map DeBrujin TypeVariable) ': effs) NType
317+ instantiate' x@(NTypeVariable _) = return x
318+ instantiate' x@(NAtomic _) = return x
319+ instantiate' (NBrujin db) = NTypeVariable <$> freshInst db
320+ instantiate' (x :-> y) = (:->) <$> instantiate' x <*> instantiate' y
321+ instantiate' (List x) = List <$> instantiate' x
322+ instantiate' (NAttrSet xs) = NAttrSet <$> traverse instantiate' xs
323+
324+ freshInst :: DeBrujin -> Eff (State (Map DeBrujin TypeVariable) ': effs) TypeVariable
325+ freshInst db = do
326+ gets (M.lookup db) >>= \case
327+ Just t -> return t
328+ Nothing -> do
329+ t <- freshSrc
330+ modify (M.insert db t)
331+ return t
332+
308333infer :: NExprLoc -> InferM NType
309334infer (Fix (Compose (Ann src x))) = runReader src $ case x of
310335 NConstant a -> return . NAtomic $ case a of
@@ -319,6 +344,7 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
319344 NSym var ->
320345 get @VariableMap
321346 >>= maybe (NTypeVariable <$> throwSrcTV (UndefinedVariable var)) return . M.lookup var
347+ >>= instantiate -- I have no idea if this covers all cases.
322348 NList xs -> do
323349 xs' <- traverse infer xs
324350 traverse_ tell . fmap (uncurry (:~)) $ zip xs' (tail xs')
test/golden/importless/nuget.txtnew file+1
@@ -0,0 +1 @@
1+∀ α. { fetchurl = { name = String; sha256 = String; url = String } -> α } -> [{ name = String; sha256 = String; url = String; version = String }]
test/golden/importless/require_exceptions.txtnew file+1
@@ -0,0 +1 @@
1+{ CFPropertyList = [String]; RubyInline = [String]; ZenTest = [String]; actioncable = [String]; actionmailer = [String]; actionpack = [String]; actionview = [String]; activejob = [String]; activemodel = [String]; activerecord = [String]; activestorage = [String]; activesupport = [String]; atk = [String]; cocoapods-acknowledgements = [String]; cocoapods-art = [String]; cocoapods-browser = [String]; cocoapods-bugsnag = String; cocoapods-check = String; cocoapods-clean = [String]; cocoapods-coverage = [String]; cocoapods-deintegrate = ∀ α. α; cocoapods-dependencies = [String]; cocoapods-deploy = String; cocoapods-disable-podfile-validations = String; cocoapods-generate = String; cocoapods-git_url_rewriter = String; cocoapods-keys = ∀ α. α; cocoapods-open = [String]; cocoapods-packager = [String]; cocoapods-packager-pro = ∀ α. α; cocoapods-plugins = [String]; cocoapods-sorted-search = ∀ α. α; cocoapods-stats = [String]; cocoapods-testing = [String]; cocoapods-trunk = [String]; cocoapods-try = [String]; cocoapods-try-release-fix = String; digest-sha3 = [String]; ffi-compiler = [String]; fog-core = [String]; fog-dnsimple = [String]; fog-json = [String]; forwardable-extended = [String]; gdk_pixbuf2 = [String]; gitlab-markup = [String]; gobject-introspection = [String]; gtk2 = ∀ α. α; idn-ruby = [String]; jekyll-sass-converter = ∀ α. α; libxml-ruby = [String]; multipart-post = [String]; nap = [String]; net-scp = [String]; net-ssh = [String]; nio4r = [String]; osx_keychain = ∀ α. α; ovirt-engine-sdk = [String]; pango = [String]; rack-test = [String]; railties = [String]; rspec-core = [String]; rspec-expectations = [String]; rspec-mocks = [String]; rspec-support = [String]; ruby-libvirt = [String]; ruby-lxc = [String]; ruby-macho = [String]; ruby-terminfo = [String]; rubyzip = [String]; sequel_pg = [String]; simplecov-html = ∀ α. α; sinatra = [String]; sprockets-rails = [String]; taglib-ruby = [String]; unicode-display_width = [String]; websocket-driver = [String]; websocket-extensions = [String] }
test/golden/importless/xsa-patches.txtnew file+1
@@ -0,0 +1 @@
1+∀ α. { fetchpatch = { sha256 = String; url = String } -> α } -> { XSA_190 = { name = String; sha256 = String }; XSA_191 = { name = String; sha256 = String }; XSA_192 = { name = String; sha256 = String }; XSA_193 = { name = String; sha256 = String }; XSA_195 = { name = String; sha256 = String }; XSA_196 = [{ name = String; sha256 = String }]; XSA_198 = { name = String; sha256 = String }; XSA_200 = { name = String; sha256 = String }; XSA_202_45 = { name = String; sha256 = String }; XSA_204_45 = { name = String; sha256 = String }; XSA_206_45 = [{ name = String; sha256 = String }]; XSA_207 = { name = String; sha256 = String }; XSA_212 = { name = String; sha256 = String }; XSA_213_45 = { name = String; sha256 = String }; XSA_214 = { name = String; sha256 = String }; XSA_215 = { name = String; sha256 = String }; XSA_217_45 = { name = String; sha256 = String }; XSA_218_45 = [{ name = String; sha256 = String }]; XSA_219_45 = { name = String; sha256 = String }; XSA_220_45 = { name = String; sha256 = String }; XSA_221 = { name = String; sha256 = String }; XSA_222_45 = [{ name = String; sha256 = String }]; XSA_223 = { name = String; sha256 = String }; XSA_224_45 = [{ name = String; sha256 = String }]; XSA_226_45 = [{ name = String; sha256 = String }]; XSA_227_45 = { name = String; sha256 = String }; XSA_230 = { name = String; sha256 = String }; XSA_231_45 = { name = String; sha256 = String }; XSA_232 = { name = String; sha256 = String }; XSA_233 = { name = String; sha256 = String }; XSA_234_45 = { name = String; sha256 = String }; XSA_235_45 = { name = String; sha256 = String }; XSA_236_45 = { name = String; sha256 = String }; XSA_237_45 = [{ name = String; sha256 = String }]; XSA_238_45 = { name = String; sha256 = String }; XSA_239_45 = { name = String; sha256 = String }; XSA_240_45 = [{ name = String; sha256 = String }]; XSA_241 = { name = String; sha256 = String }; XSA_242 = { name = String; sha256 = String }; XSA_243_45 = [{ name = String; sha256 = String }]; XSA_244_45 = { name = String; sha256 = String }; XSA_245 = [{ name = String; sha256 = String }]; XSA_246_45 = [{ name = String; sha256 = String }]; XSA_247_45 = [{ name = String; sha256 = String }]; XSA_248_45 = [{ name = String; sha256 = String }]; XSA_249 = [{ name = String; sha256 = String }]; XSA_250_45 = [{ name = String; sha256 = String }]; XSA_251_45 = [{ name = String; sha256 = String }] }