> On Dec 14, 2016, at 10:07 AM, Carter Schonwald <carter.schonw...@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 _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
