Fix Newtype instance in test code

[JordanMartinez]

Description of the change

Fixes the Newtype instance in the test code that currently prevents CI from passing.

---

Checklist:

• Added the change to the changelog's "Unreleased" section with a reference to this PR (e.g. "- Made a change (#0000)")
• Linked any existing issues or proposals that this pull request should close
• Updated or added relevant documentation
• Added a test for the contribution (if applicable)

[JordanMartinez]

CI fails because fun deps don't propagate:

[1/1 NoInstanceFound] test/Main.purs:12:1

      v
  12  instance newtypeRecordNewtype ::
  13    TypeEquals inner { message :: String }
  14      => Newtype RecordNewtype inner
                                       ^
  
  No type class instance was found for
  
    Prim.Coerce.Coercible inner0
                          { message :: String
                          }
  
  while solving type class constraint
  
    Prim.Coerce.Coercible RecordNewtype
                          inner0
  
  while checking that expression #dict Coercible
    has type Coercible$Dict @Type RecordNewtype inner0
  in value declaration newtypeRecordNewtype
  
  where inner0 is a rigid type variable
          bound at (line 0, column 0 - line 0, column 0)

           Src   Lib   All
Warnings   0     0     0  
Errors     1     0     1  

[MonoidMusician]

I think you just need to add that constraint to the constraints for the instance. I don’t foresee any issues with that ...

Actually, did we drop the restriction on rows? Might be able to remove the type equality constraint and just replace inner with the record, if we did.

[JordanMartinez]

I think you just need to add that constraint to the constraints for the instance. I don’t foresee any issues with that ...

Can you clarify?

Also, is this test still the best way to test this library?

[MonoidMusician]

@JordanMartinez I PRd your branch with my idea but I think we probably need to test more (especially since we got rid of the methods): https://github.com/JordanMartinez/purescript-type-equality/pull/1

[JordanMartinez]

I've merged your changes.

Just a thought, but since we need the Coercible constraint to get the code to compile, what if we added it as a superclass to TypeEquals? If so, then do we still need the From and To newtypes?

class TypeEquals :: forall k. k -> k -> Constraint
class Coercible a b <= TypeEquals a b | a -> b, b -> a where
  proof :: forall p. p a -> p b

instance refl :: TypeEquals a a where
  proof a = a

to :: forall a b. TypeEquals a b => a -> b
to = coerce

from :: forall a b. TypeEquals a b => b -> a
from = coerce

Regardless, I feel like we need more tests to verify this code works properly.

[hdgarrood]

Using coerce for the implementations feels wrong to me, but I think adding the superclass is worth considering so that we don't break all existing Newtype instances for record newtypes.

[hdgarrood]

I don't think we need more tests - this is a case where we should be trusting the compiler, I think.

[JordanMartinez]

Ok. I've pushed the changes.

[hdgarrood]

Looks good to me! I’d like to hear from @kl0tl before merging though.

[hdgarrood]

Incidentally I think using coerce feels wrong to me because it would allow you to write those functions in such a way that wouldn’t ensure that a and b are actually the exact same type, whereas the current implementation does ensure this.

[kl0tl]

Nominally equal types are also representationally equal, so since TypeEquals embodies nominal equality this makes sense to me!

I don’t think implementing to and from with coerce would be wrong per se because the TypeEquals a b constraint doesn’t hold unless the types are really the same, but it might be worthwhile for those functions to serve as an example of how to actually use the type equality proof?

[kl0tl]

There’s no need for those parens now that the Coercible constraint is introduced by TypeEquals itself.

[JordanMartinez]

Done.

[hdgarrood]

Yeah exactly, I think we should be using the type equality proof here for dogfooding reasons as well.

[JordanMartinez]

Pretty sure this is ready to merge.