Re: Heterogeneous equality

> On Jul 5, 2017, at 5:23 PM, Wolfgang Jeltsch wrote: > > Hi! > > The base package contains the module Data.Type.Equality, which contains > the type (:~:) for homogeneous equality. I was a bit surprised that > there is no type for heterogeneous equality there. Is

Re: Trouble with injective type families

> On Wed Jul 5 14:16:10 UTC 2017, Richard Eisenberg wrote: > I'd like to add that the reason we never extended System FC > with support for injectivity is that the proof of soundness > of doing so has remained elusive. Thank you Richard, Simon. IIRC the original FDs through CHRs paper did think