<div dir="auto"><div>To be more specific about the ad hoc equality option, I'm thinking about something like this (if it doesn't compile, I'm sure something similar will):</div><div dir="auto"><br></div><div dir="auto"><div dir="auto" style="font-family:sans-serif">type family (a :: k) == (b :: k) :: Bool</div><div dir="auto" style="font-family:sans-serif">infix 4 ==</div><div dir="auto" style="font-family:sans-serif"><br></div><div dir="auto" style="font-family:sans-serif"><div dir="auto">type family Equal (k :: Type) (a :: k) (b :: k) where</div><div dir="auto"><span style="white-space:pre-wrap"> </span> Equal k ((f :: j -> k) (a :: j)) ((g :: j -> k) (b :: j)) =</div><div dir="auto"><span style="white-space:pre-wrap"> </span> Equal (j -> k) f g && (a == b)</div><div dir="auto"><span style="white-space:pre-wrap"> </span> Equal k a a = 'True</div><div dir="auto"><span style="white-space:pre-wrap"> </span> Equal k a b = 'False</div><div dir="auto"><br></div><div dir="auto">type instance (a :: Type) == b = Equal Type a b</div><div dir="auto">type instance (a :: Maybe k) == b = Equal Type a b</div><div dir="auto">....</div><div dir="auto"><br></div><div dir="auto">So for example, we'd get</div><div dir="auto"><br></div><div dir="auto">'Just (x :: k) == 'Just y</div><div dir="auto">=</div><div dir="auto">Equal (k -> Maybe k) 'Just && x == y</div><div dir="auto">=</div><div dir="auto">x == y</div></div><div class="gmail_extra" dir="auto"><br><div class="gmail_quote">On Aug 10, 2017 12:29 AM, "David Feuer" <<a href="mailto:david.feuer@gmail.com">david.feuer@gmail.com</a>> wrote:<br type="attribution"><blockquote class="quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto">The (==) type family in Data.Type.Equality was designed largely to calculate structural equality of types. However, limitations of GHC's type system at the type prevented this from being fully realized. Today, with TypeInType, we can actually do it, replacing the boatload of ad hoc instances like so:<div dir="auto"><br></div><div dir="auto"><div dir="auto">type (a :: k) == (b :: k) = Equal k a b</div><div dir="auto">infix 4 ==</div><div dir="auto"><br></div><div dir="auto"><div dir="auto">type family Equal (k :: Type) (a :: k) (b :: k) where</div><div dir="auto"><span style="white-space:pre-wrap"> </span> Equal k ((f :: j -> k) (a :: j)) ((g :: j -> k) (b :: j)) =</div><div dir="auto"><span style="white-space:pre-wrap"> </span> Equal (j -> k) f g && Equal j a b</div><div dir="auto"><span style="white-space:pre-wrap"> </span> Equal k a a = 'True</div><div dir="auto"><span style="white-space:pre-wrap"> </span> Equal k a b = 'False</div><div dir="auto"><br></div><div dir="auto">This == behaves in a much more uniform way than the current one. I see two potential causes for complaint:</div><div dir="auto"><br></div><div dir="auto">1. For types of kind *, the new version will sometimes fail to reduce when the old one succeeded (and vice versa). For example, GHC currently accepts</div><div dir="auto"><br></div><div dir="auto">eqeq :: forall (a :: *). proxy a -> (a == a) :~: 'True</div><div dir="auto">eqeq _ = Refl</div><div dir="auto"><br></div><div dir="auto">while the proposed version does not.</div><div dir="auto"><br></div><div dir="auto">2. Some users may want non-structural equality on their types for some reason. The only example in base is</div><div dir="auto"><br></div><div dir="auto">type instance (a :: ()) == (b :: ()) = 'True</div><div dir="auto"><br></div><div dir="auto">which consists two types of kind () the same even if they're stuck types. But perhaps someone wants to implement a non-trivial type-level data structure with a special notion of equality.</div><div dir="auto"><br></div><div dir="auto"><br></div><div dir="auto">I don't think (1) is really worth worrying too much about. For (2), if users want to have control, we could at least use a mechanism similar to the above to make the obvious instances easier to write.</div></div></div></div>
</blockquote></div><br></div></div></div>