Typed structural equality #154

kquick · 2023-06-07T20:44:23Z

The structuralEquality TH implementation does not witness the equality of the types involved, which can make it difficult to use for parameterized GADT types. It also cannot correctly generate the comparison slices for parameterized GADTs because there may not be wildcard cases admissable due to type equality, even if there are other constructors with other resulting types.

The impact should be minimal, although it may require the introduction of the ScopedTypeParameters pragma in sources importing and using this code.

Without the change to structuralEquality, the new tests would result in errors like the following: test/Test/TH.hs:51:11: error: • Couldn't match type ‘a1’ with ‘(:~:) @{k0} a0 a0’ Expected: Maybe a1 Actual: Maybe ((:~:) @{k0} a0 a0) • ‘a1’ is untouchable inside the constraints: "int" ~ "int" bound by a pattern with constructor: T3_Int :: Int -> T3 "int", in a case alternative at test/Test/TH.hs:51:11-41 • In the expression: Just Refl In the expression: if (x1_ab5y == y1_ab5z) then Just Refl else Nothing In a case alternative: T3_Int y1_ab5z -> if (x1_ab5y == y1_ab5z) then Just Refl else Nothing | 51 | (==) = $(structuralEquality [t|T3|] []) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Older GHC versions do not allow unary tuples.

When generating `structuralEquality` or `structuralTypeEquality`, the former is used in an `Eq` scenario for `(==) :: a -> a -> Bool` and so if there is a GADT definition like the following:] data T1 a where T1_Int :: Int -> T1 Int T1_Char :: Char -> T1 Char then the `(==)` function will only admit `T1_Int` constructors or `T1_Char` constructors but not both. However, `TestEquality` will parameterize over the GADT type parameter and does not require them to match. As a result, when generating the splice for comparison: \x y -> case x of T1_Int -> case y of T1_Int -> ... _ -> False -- << HERE T1_Char -> case y of T1_Char -> ... _ -> False -- << AND HERE that splice is fine for `TestEquality`, but because the types must match for `Eq` then the two wildcard clauses marked by HERE comments above are superfluous and cause warnings/errors. There may be other explicit matchers (e.g. if T1 also had a `T1_Nat :: Nat -> T1 Int` constructor) which will be needed, but the wildcard should only be present for testEquality. This patch makes the adjustment to allow for the differences in the structuralEquality and structuralTypeEquality definitions, along with some tests to demonstrate/exercise those changes.

RyanGlScott

Reading the PR description, it wasn't obvious to me why this change was necessary in the first place. Here is my attempt to describe the issue, after looking at the -ddump-splices output a bit.

When you use structuralTypeEquality, like in this example:

data T a where
  MkT1 :: T Int
  MkT2 :: T Bool

instance TestEquality T where
  testEquality :: T a -> T b -> Maybe (a :~: b)
  testEquality = $(structuralTypeEquality [t|T|] [])

Then you will generate code involving GADT pattern-matching. This can interact poorly with type inference in general, but because the type of testEquality mentions Maybe (a :~: b) in its return type, this provides enough information to allow the GADT pattern matches to type-check.

structuralEquality is a minor variation of structuralTypeEquality. If you write this:

instance TestEquality T where
  testEquality :: T a -> T a -> Bool
  testEquality = $(structuralEquality [t|T|] [])

It is equivalent to writing this:

instance TestEquality T where
  testEquality :: T a -> T a -> Bool
  testEquality = isJust $(structuralTypeEquality [t|T|] [])

This is very similar to the previous example, but with a key difference: the return type is now Bool, which no longer mentions any of the type variables. As a result, GHC's type inference has no way to know what the overall type of the generated GADT pattern matches should be, and therefore the generated code will fail to type-check. (Concretely, GHC will complain that that the a in T a is untouchable.)

One way to fix this issue is to add an explicit type ascription to the generated case expression that makes the return type of the case clear. This requires binding type variables, as they may not yet be in scope:

instance TestEquality T where
  testEquality :: T a -> T a -> Bool
  testEquality = isJust (\arg1 arg2 -> (\(x :: T a) (y :: T b) -> case (x, y) of { ... } :: Maybe (a :~: b)) arg1 arg2)

This is the approach taken in this PR.

RyanGlScott · 2023-06-08T07:58:28Z

Changelog.md

+
+  * Updates Data.Parameterized.TH.GADT.structuralEquality to add type assertions
+    to cover all type parameters.  This change may require the addition of the
+    @ScopedTypeVariables@ pragma to modules importing this code.


This uses markdown rather than Haddock formatting, so use backticks instead:

Suggested change

@ScopedTypeVariables@ pragma to modules importing this code.

`ScopedTypeVariables` pragma to modules importing this code.

RyanGlScott · 2023-06-08T07:58:46Z

Changelog.md

@@ -2,6 +2,12 @@

 ## next -- *TBA*

+## 2.1.6.0.100
+
+  * Updates Data.Parameterized.TH.GADT.structuralEquality to add type assertions


Suggested change

* Updates Data.Parameterized.TH.GADT.structuralEquality to add type assertions

* Updates `Data.Parameterized.TH.GADT.structuralEquality` to add type assertions

RyanGlScott · 2023-06-08T08:52:08Z