Explicit inequality evidence

[Richard Eisenberg]

> On Dec 14, 2016, at 10:07 AM, Carter Schonwald <carter.schonwald at gmail.com> wrote:
> 
> Possibly naive question: do we have decidable inequality in a meta theoretical sense? I feel like we have definite equality and fuzzy might not always be equal but could be for polymorphic types. And that definite inequality on non polymorphic terms is a lot smaller than what folks likely want?

Not sure what you mean here. FC/Core has a definitional equality which is decidable (and must be). And if definitional equality is decidable, it follows that definitional inequality is decidable. On the other hand, what we are talking about in this thread is *propositional* inequality -- that is, an inequality supported by a proof. Propositional equality must be a larger relation than definitional equality: this is what the Refl constructor, or <t> in the Greek, shows. It then follows that propositional inequality must be smaller than definitional inequality. This is a Good Thing, because F Int and Bool are definitionally inequal, but we don't want them to be propositionally inequal.

Propositional inequality is almost surely undecidable, because of looping type families (at least). But that's OK -- propositional equality is also undecidable, and that hasn't slowed us down. :)

Richard