I'm trying to use the generic graph library in typed racket, by importing it with require/typed, but I keep getting these weird long errors. Has anyone managed to get the type checker to cooperate with the generic graph library?
#lang typed/racket
(require/typed graph
[#:opaque Graph graph?]
[unweighted-graph/undirected ((Listof (List Any Any)) -> Graph)]
[add-edge! (Graph Any Any -> Void)])
(define g : Graph (unweighted-graph/undirected '((1 2) (1 3))))
(add-edge! g 2 3)
graph?: contract violation
any-wrap/c: Unable to protect opaque value passed as `Any`
value: #<unweighted-graph>
This warning will become an error in a future release.
in: the 1st argument of
a part of the or/c of
(or/c
struct-predicate-procedure?/c
(-> Any boolean?))
contract from: (interface for graph?)
This isn't ideal, but there is a workaround:
#lang typed/racket
(module wrapper racket
(provide graph? unweighted-graph/undirected add-edge!)
(require (prefix-in g: graph))
(struct graph [g]) ; struct generates the predicate
(define (unweighted-graph/undirected es) ; wrap output graph
(graph (g:unweighted-graph/undirected es)))
(define (add-edge! g a b) ; unwrap input graph
(g:add-edge! (graph-g g) a b)))
(require/typed 'wrapper
[#:opaque Graph graph?]
[unweighted-graph/undirected ((Listof (List Any Any)) -> Graph)]
[add-edge! (Graph Any Any -> Void)])
(define g : Graph (unweighted-graph/undirected '((1 2) (1 3))))
(add-edge! g 2 3)
When Typed Racket require/typed sees #:opaque, it still needs to treat the predicate you gave, graph? as untyped code. But it also needs to use that predicate from untyped code to guard values on the typed-untyped boundary. The graph? predicate has the type (-> Any Boolean), so when typed racket calls it with a value from typed code it's passing it with the type Any. However, if before this it had a more specific type that involves inputs that must be typed, it still needs to guard against untyped code "using it" in the wrong way, or providing bad untyped inputs.
Adding an opaque struct sidesteps this by making a new graph? predicate that doesn't need to "look inside" the value in the same way.