search

dwango / fialyzer

[WIP] Faster Implementation of Dialyzer
https://dwango.github.io/fialyzer/
Apache License 2.0
56 stars 8 forks source link

An unnecessary constraint for the derivation rule [MfaExpr] #172

Closed yoshihiro503 closed 5 years ago

yoshihiro503 commented 5 years ago

In the rule

A ⊢ m : τm, Cm   A ⊢ f : τf, Cf   A ⊢ a : τa, Ca
------------------------------------------------------------------------------------[MFAEXPR]
A ⊢ fun m:f/a : τ, (τ ⊆ any()) ∧ (τm ⊆ atom()) ∧ (τf ⊆ atom()) ∧ (τa ⊆ number()) ∧ Cm ∧ Cf ∧ Ca

, the constraint (τ ⊆ any()) is unnecessary. Whether it is with or without this, it is the same.

see : https://github.com/dwango/fialyzer/pull/164#discussion_r252184968