subtyping optional keywords in HMaps

[claire alvis]

Is this me not understanding subtyping or is this an error in core.typed?
(version 0.3.22)

(ns test.core

(:require [clojure.core.typed :as t]))

(t/defalias XYZMap
(t/TFn [[x :variance :covariant :< Number]
[y :variance :covariant :< Number]
[z :variance :covariant :< Number]]
(t/HMap :complete? true
:mandatory {:x x
:y (t/Option y)}
:optional {:z z})))

(t/defn x-getter
[m :- (XYZMap Integer Integer Integer)] :- Integer
(:x m))

(t/defn y-getter
[m :- (XYZMap Integer Integer Integer)] :- (t/Option Integer)
(:y m))

(t/defn z-getter
[m :- (XYZMap Integer Integer Integer)] :- (t/Option Integer)
(:z m))


I would expect all of these functions to be well typed, but I get an error
only in the type of z-getter:

Type Error (test/core.clj:23:3) Type mismatch:

Expected: (t/Option Integer)

Actual: (t/U z nil)
in: (:z m)

ExceptionInfo Type Checker: Found 1 error clojure.core/ex-info
(core.clj:4593)


I would think the instantiation of z to Integer in the argument to z-getter
would be enough to
prove that the access returns "either an Integer or nil".


Claire

[Ambrose Bonnaire-Sergeant]

Hi Claire,

I bet the substitution of type variables doesn't work under optional
entries. That would explain the existence of z in the final type error.

Please submit a ticket.

Thanks,
Ambrose
On 13 Apr 2016 15:36, "claire alvis" <***@gmail.com> wrote:

Is this me not understanding subtyping or is this an error in core.typed?
(version 0.3.22)

(ns test.core

(:require [clojure.core.typed :as t]))

(t/defalias XYZMap
(t/TFn [[x :variance :covariant :< Number]
[y :variance :covariant :< Number]
[z :variance :covariant :< Number]]
(t/HMap :complete? true
:mandatory {:x x
:y (t/Option y)}
:optional {:z z})))

(t/defn x-getter
[m :- (XYZMap Integer Integer Integer)] :- Integer
(:x m))

(t/defn y-getter
[m :- (XYZMap Integer Integer Integer)] :- (t/Option Integer)
(:y m))

(t/defn z-getter
[m :- (XYZMap Integer Integer Integer)] :- (t/Option Integer)
(:z m))


I would expect all of these functions to be well typed, but I get an error
only in the type of z-getter:

Type Error (test/core.clj:23:3) Type mismatch:

Expected: (t/Option Integer)

Actual: (t/U z nil)
in: (:z m)

ExceptionInfo Type Checker: Found 1 error clojure.core/ex-info
(core.clj:4593)


I would think the instantiation of z to Integer in the argument to z-getter
would be enough to
prove that the access returns "either an Integer or nil".


Claire