fix: False positive in type equality #75
Conversation
There was a problem hiding this comment.
Ooops, my bad, but I'm puzzled why this doesn't work.
ends are both
data End = InEnd InPort | ExEnd OutPort
deriving (Eq, Ord)
where
data OutPort = Ex Name Int deriving (Eq, Ord, Show)
data InPort = In Name Int deriving (Eq, Ord, Show)
So I believed the previous code would be true only for variables being the same port (Int) of the same node (Name). Obviously that isn't what happens (I agree that without this fix your "golden test" compiles, when it shouldn't) but why?
|
Both of the metavariables in the example are defined in terms of the |
| @@ -159,6 +160,31 @@ data Val :: N -> Type where | |||
| VApp :: VVar n -> Bwd (Val n) -> Val n | |||
| VSum :: MODEY m => Modey m -> [Some (Ro m n)] -> Val n -- (Hugr-like) Sum types | |||
|
|
|||
| -- Define a naive version of equality, which only says whether the data | |||
| -- structures are on-the-node equal | |||
| instance Eq (Val n) where | |||
There was a problem hiding this comment.
Is it not possible to derive Eq?
There was a problem hiding this comment.
No, because we have things like VFun with an existential mode, which means GHC has to test that the modes are equal on both sides before it can tell that the CTys actually have the same type!
There was a problem hiding this comment.
Also note there's no Eq for VSum because that one is very tricky, and it's only produced by the compiler so I doubt we'll need to test equality for it (I'll add a comment saying this)
There was a problem hiding this comment.
Do we even use VSum? I thought we got rid of it?
There was a problem hiding this comment.
😮 I didn't realise we stopped using it
There was a problem hiding this comment.
#76 saves me having to add a comment
Co-authored-by: Mark Koch <[email protected]>
When comparing types, the easy case is not when the variables are the same, but rather when the haskell representations of the values are equal! I've added a test case that would have typechecked before to demonstrate.