On Mon, Dec 16, 2019 at 01:42:39AM -0500, Viktor Dukhovni wrote:
Not sure where to post about this, and it has likely been noted elsewhere already, but reading through the report I see in Section 3.17.2
• Consider the following declarations:
newtype N = N Bool data D = D !Bool
These examples illustrate the difference in pattern matching between types defined by data and newtype:
(\ (N True) -> True) ⊥ ⇒ ⊥ (\ (D True) -> True) ⊥ ⇒ ⊥ (\ ~(D True) -> True) ⊥ ⇒ True
Additional examples may be found in Section 4.2.3.
But unlike the examples in 4.2.3, which do show differences between "newtype" and "data", the above does not seem to show any actual difference. For that the pattern after the constructor would I believe have to be irrefutable, which "True" is not.
I think what you're saying is that this doesn't show a difference because (\ ~(N True) -> True) ⊥ ⇒ True