FStarLang/FStar

Failure of type inference with repeated variables

Open

#1.007 geöffnet am 21. Apr. 2017

Auf GitHub ansehen
 (3 Kommentare) (0 Reaktionen) (1 zugewiesene Person)F* (258 Forks)auto 404
area/proof-assistantcomponent/typecheckercomponent/unifiergood first issuekind/enhancementmilestone/everest-v1

Repository-Metriken

Stars
 (3.068 Stars)
PR-Merge-Metriken
 (PR-Metriken ausstehend)

Beschreibung

Lax-typechecking the following snippet

let f (x y : int) (w:(b:bool & (if b then equals x y else equals y x))) =
  match w with
  | (| b, Refl |) -> ()

fails with the error

(Error) (equals (?26524 x y w b) (?26524 x y w b)) is not a subtype of the expected type (match b with
	| true  -> (equals x y)
	|_  -> (equals y x))

Contributor Guide

Research-Richtung
Untersuchen Sie die Behandlung von wiederholten Variablen im Pattern Matching durch den Typprüfer, insbesondere die Inferenz von Gleichungen in abhängigen Pattern Matches.
Tech Stack
Keine
Domain
compilers
Issue Type
Fehler
SchwierigkeitGeschätzte Implementierungsschwierigkeit für neue Contributors, von 1 für sehr kleine Änderungen bis 5 für Expertenarbeit.
4
Geschätzte ZeitEin grober Zeitrahmen, um zu recherchieren, zu implementieren, zu testen und einen Pull Request vorzubereiten.
3-5 Tage
AktivitätsstatusWie verfügbar das Issue gerade wirkt: frisch, aktiv, stale, blockiert oder wartet auf Maintainer-Input.
Aktiv
KlarheitWie klar das Issue die erwartete Änderung, Akzeptanzkriterien und den nächsten Schritt erklärt.
Klar
Voraussetzungen
Git
EinsteigerfreundlichkeitEin Score von 1 bis 100, der schätzt, wie zugänglich dieses Issue für First-Time Contributors ist.
40