On Tue, Dec 13, 2016 at 12:49 AM, Oleg Grenrus <oleg.gren...@iki.fi> wrote: > First the bike shedding: I’d prefer /~ and :/~:.
Those are indeed better. > new Typeable [1] would actually provide heterogenous equality: > > eqTypeRep' :: forall k1 k2 (a :: k1) (b :: k2). > TypeRep a -> TypeRep b -> Maybe (a :~~: b) > > And this one is tricky, should it be: > > eqTypeRep' :: forall k1 k2 (a :: k1) (b :: k2). > TypeRep a -> TypeRep b -> > Either (Either (k1 :/~: k2) (a :/~: b)) (a :~~: b) > > i.e. how kind inequality would work? I don't know. It sounds like some details of how kinds are expressed in TypeRep might still be a bit uncertain, but I'm not tuned in. Maybe we should punt and use heterogeneous inequality? That's over my head. > I'm not sure about propagation rules, with inequality you have to be *very* > careful! > > irreflexivity, x /~ x and symmetry x /~ y <=> y /~ x are clear. > > I assume that in your rules, variables are not type families, otherwise > > x /~ y => f x /~ f y doesn't hold if `f` isn't injective. (e.g. type family F > x where F x = ()) > other direction is true though. I was definitely imagining them as first-class types; your point that f x /~ f y => x /~ y even if f is a type family is an excellent one. > Also: > > f x ~ a -> b, is true with f ~ (->) a, x ~ b. Whoops! Yeah, I momentarily forgot that (->) is a constructor. Just leave out that bogus piece. Thanks, David Feuer _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs