Remove certifiers for Opaque and Refinement types

Syntax certifiers are now deprecated. This change
should have no effect on the types.

original commit: 0e02b7e368a674582c81f5df163ce32b79ade015

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt

@@ -322,7 +322,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
     (pattern #:name-exists))
   (syntax-parse stx
     [(_ ty:id pred:id lib (~optional ne:name-exists-kw) ...)
-     (register-type-name #'ty (make-Opaque #'pred (syntax-local-certifier)))
+     (register-type-name #'ty (make-Opaque #'pred))
      (with-syntax ([hidden (generate-temporary #'pred)])
        (quasisyntax/loc stx
          (begin

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/init-envs.rkt

@@ -57,10 +57,9 @@
                    ,(sub flds) ,(sub proc) ,(sub poly?)
                    (quote-syntax ,pred-id))]
     [(App: rator rands stx) `(make-App ,(sub rator) ,(sub rands) (quote-syntax ,stx))]
-    [(Opaque: pred cert) `(make-Opaque (quote-syntax ,pred) (syntax-local-certifier))]
-    [(Refinement: parent pred cert) `(make-Refinement ,(sub parent)
-                                                      (quote-syntax ,pred)
-                                                      (syntax-local-certifier))]
+    [(Opaque: pred) `(make-Opaque (quote-syntax ,pred))]
+    [(Refinement: parent pred) `(make-Refinement ,(sub parent)
+                                                 (quote-syntax ,pred))]
     [(Mu-name: n b) `(make-Mu ,(sub n) ,(sub b))]
     [(Poly-names: ns b) `(make-Poly (list ,@(map sub ns)) ,(sub b))]
     [(PolyDots-names: ns b) `(make-PolyDots (list ,@(map sub ns)) ,(sub b))]

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt

@@ -415,7 +415,7 @@
                (nevermind))]
 
           ;; refinements are erased to their bound
-          [((Refinement: S _ _) T)
+          [((Refinement: S _) T)
            (cg S T)]
 
           ;; variables that are in X and should be constrained

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/parse-type.rkt

@@ -182,7 +182,7 @@
        (add-disappeared-use #'kw)
        (match (lookup-type/lexical #'p?)
          [(and t (Function: (list (arr: (list dom) _ #f #f '()))))
-          (make-Refinement dom #'p? (syntax-local-certifier))]
+          (make-Refinement dom #'p?)]
          [t (tc-error "cannot declare refinement for non-predicate ~a" t)])]
       [((~and kw t:Struct) t)
        (add-disappeared-use #'kw)
@@ -264,7 +264,7 @@
        (parse-all-type stx)]
       [((~and kw t:Opaque) p?)
        (add-disappeared-use #'kw)
-       (make-Opaque #'p? (syntax-local-certifier))]
+       (make-Opaque #'p?)]
       [((~and kw t:Parameter) t)
        (let ([ty (parse-type #'t)])
          (add-disappeared-use #'kw)

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt

@@ -338,8 +338,8 @@
         [(== t:-Number type-equal?) #'(flat-named-contract 'Number number?)]
 
         [(Base: sym cnt _ _ _) #`(flat-named-contract '#,sym (flat-contract-predicate #,cnt))]
-        [(Refinement: par p? cert)
-         #`(and/c #,(t->c par) (flat-contract #,(cert p?)))]
+        [(Refinement: par p?)
+         #`(and/c #,(t->c par) (flat-contract #,p?))]
         [(Union: elems)
          (let-values ([(vars notvars) (partition F? elems)])
            (unless (>= 1 (length vars)) (exit (fail)))
@@ -364,8 +364,8 @@
         [(Promise: t)
          (set-chaperone!)
          #`(promise/c #,(t->c t))]
-        [(Opaque: p? cert)
-         #`(flat-named-contract (quote #,(syntax-e p?)) #,(cert p?))]
+        [(Opaque: p?)
+         #`(flat-named-contract (quote #,(syntax-e p?)) #,p?)]
         [(Continuation-Mark-Keyof: t)
          (set-chaperone!)
          #`(continuation-mark-key/c #,(t->c/both t))]

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/type-rep.rkt

@@ -237,8 +237,7 @@
                 (*PolyDots n (add-scopes n (type-rec-id body*))))])
 
 ;; pred : identifier
-;; cert : syntax certifier
-(def-type Opaque ([pred identifier?] [cert procedure?])
+(def-type Opaque ([pred identifier?])
   [#:intern (hash-id pred)] [#:frees #f] [#:fold-rhs #:base] [#:key pred])
 
 ;; kw : keyword?
@@ -336,7 +335,6 @@
 ;; poly? : is this type polymorphicly variant
 ;;         If not, then the predicate is enough for higher order checks
 ;; pred-id : identifier for the predicate of the struct
-;; cert : syntax certifier for pred-id
 ;; acc-ids : names of the accessors
 ;; maker-id : name of the constructor
 (def-type Struct ([name identifier?]
@@ -418,10 +416,10 @@
 (def-type Hashtable ([key Type/c] [value Type/c]) [#:key 'hash]
   [#:frees (λ (f) (combine-frees (list (make-invariant (f key)) (make-invariant (f value)))))])
 
-(def-type Refinement ([parent Type/c] [pred identifier?] [cert procedure?])
+(def-type Refinement ([parent Type/c] [pred identifier?])
   [#:key (Type-key parent)]
   [#:intern (list (Rep-seq parent) (hash-id pred))]
-  [#:fold-rhs (*Refinement (type-rec-id parent) pred cert)]
+  [#:fold-rhs (*Refinement (type-rec-id parent) pred)]
   [#:frees (λ (f) (f parent))])
 
 

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt

@@ -118,7 +118,7 @@
               [(and t (Function: (list (arr: (list dom) (Values: (list (Result: rng _ _))) #f #f '()))))
                (let ([new-t (make-pred-ty (list dom)
                                           rng
-                                          (make-Refinement dom #'pred (syntax-local-certifier)))])
+                                          (make-Refinement dom #'pred))])
                  (register-type #'pred new-t))
                (list)]
               [t (tc-error "cannot declare refinement for non-predicate ~a" t)])]

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt

@@ -299,7 +299,7 @@
     [(? tuple? t)
      (fp "~a" (cons 'List (tuple-elems t)))]
     [(Base: n cnt _ _ _) (fp "~s" n)]
-    [(Opaque: pred _) (fp "(Opaque ~a)" (syntax->datum pred))]
+    [(Opaque: pred) (fp "(Opaque ~a)" (syntax->datum pred))]
     [(Struct: nm       par (list (fld: t _ _) ...)       proc _ _)
      (fp "#(struct:~a ~a" nm t)
      (when proc
@@ -381,7 +381,7 @@
     [(Result: t fs (Empty:)) (fp "(~a : ~a)" t fs)]
     [(Result: t fs lo) (fp "(~a : ~a : ~a)" t fs lo)]
     [(MPair: s t) (fp "(MPairof ~a ~a)" s t)]
-    [(Refinement: parent p? _)
+    [(Refinement: parent p?)
      (fp "(Refinement ~a ~a)" parent (syntax-e p?))]
     [(Sequence: ts)
      (fp "(Sequenceof")

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/remove-intersect.rkt

@@ -33,8 +33,8 @@
          [(list _ (Univ:)) #t]
          [(list (F: _) _) #t]
          [(list _ (F: _)) #t]
-         [(list (Opaque: _ _) _) #t]
-         [(list _ (Opaque: _ _)) #t]
+         [(list (Opaque: _) _) #t]
+         [(list _ (Opaque: _)) #t]
          [(list (Name: n) (Name: n*))
           (or (free-identifier=? n n*)
               (overlap (resolve-once t1) (resolve-once t2)))]
@@ -45,8 +45,8 @@
          [(list (? Mu?) _) (overlap (unfold t1) t2)]
          [(list _ (? Mu?)) (overlap t1 (unfold t2))]
 
-         [(list (Refinement: t _ _) t2) (overlap t t2)]
-         [(list t1 (Refinement: t _ _)) (overlap t1 t)]
+         [(list (Refinement: t _) t2) (overlap t t2)]
+         [(list t1 (Refinement: t _)) (overlap t1 t)]
 
          [(list (Union: e) t)
           (ormap (lambda (t*) (overlap t* t)) e)]

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt

@@ -392,7 +392,7 @@
                  (hash-set (make-simple-substitution ns (map make-F (take ms (length ns))))
                            n-dotted (i-subst (map make-F (drop ms (length ns))))))
                (subtype* A0 (subst-all subst b1) b2)]
-              [((Refinement: par _ _) t)
+              [((Refinement: par _) t)
                (subtype* A0 par t)]
               ;; use unification to see if we can use the polytype here
               [((Poly: vs b) s)