racket / racket/typed-racket

awful refinement type error message

Open
#696 0 comments 0 reactions 1 assignee View on GitHub

@pnwamk is already working on this.

Since Apr 19, 2018.

Dominant language
Racket
Stars
575
Forks
106
Avg merge
2h 1m
Merged PRs (30d)
2

Description

Type Checker: type mismatch
  expected: (Refine
             (a : Byte)
             (and (<= a 59)
                  (<= 5 a)
                  (or (<= a 21) (<= 41 a))
                  (or (<= 19 a) (<= a 5))
                  (or (<= 59 a) (<= a 41))))
  given: SomeInts in: (case r ((a) (ann 41 SomeInts)))

For the following program:

#lang typed/racket


(define-type SomeInts
  (Refine [n : Byte] (or (= n #x05) (<= #x13 n #x15) (= n #x29) (= n #x3B))))

(: bar (-> Any SomeInts))
(define (bar r)
  (case r
    [(a) (ann #x29 SomeInts)]))

Note that adding #:with-refinements to the top line fixes the type checking issue.

Contributor guide

No contributing guide indexed for this repository

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.