#9636: Function with type error accepted -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by augustss): Replying to [comment:17 goldfire]:
Unfortunately, this, too, violates the substitution lemma. We probably want to be able to solve `(a ~ a)` with reflexivity, for ''any'' `a`. But, you're suggesting that a particular value for `a`, namely `T Bool`, will ''not'' equal itself.
I'm saying it's neither equal to itself, nor unequal to itself. `T Bool` is in some sense ill formed, so asking if it's equal to itself is nonsensical, because it's not a a type. Can you use reflexivity to conclude `Int Bool ~ Int Bool`? No, because it's an ill-formed typed. The case with `T Bool` is not as severely ill form, though. If you want to keep `T Bool` you have to have a different explanation what makes a type. Types a made from `data`, `newtype`, and `type family`. But for `type family` certain of the the types are actually equal to other existing types. But if no equation holds then it's a new (empty) type, distinct from all other types. I can go along with that explanation, but it's not very satisfactory to me. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9636#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler