#15648: Core Lint error with source-level unboxed equality -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #15209 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I can see several things here. 1. `(~#)` has a funny kind (see `prelude/TysPrim`: {{{ (~#) :: forall k1 k2. k1 -> k2 -> TYPE (TupleRep []) }}} The kind `TYPE TupleRep []` says that values of this type are represented by a zero-tuple of values; which takes zero bits. 2. Note that it does ''not'' have return kind `Constraint`. Indeed, it can't, because that would mean it had a boxed, lifted representation, since (after the type checker) `Constraint` and `Type` are the same. So it won't behave like an invisible argument, because it doesn't have kind `Constraint`. Making `(~#)` behave like `(~)` in source code would be problematic for this reason. 3. In Core, term-level variables (`Id`) are split into coercion variables (`CoVar`s) and all others; distinguished by their `IdDetails` field, and `isCoVarId`. Coercion variables can be ''bound'' in terms (say by a lambda) but, unlike other Ids, can ''occur'' only in types and coercions. The simplifier keeps them in a different environment for that reason. In short: * A variable should reply True to `isCoVarId` '''iff''' it has type `t1 ~# t2` or `t1 ~R# t2`. * A `CoVar` should occur only in types or coercions, never in a term (i.e. `Var` in Core). Lint checks for the latter, but not the former; I'll fix that. 4. This program has a non-`CoVar` bound by a lambda, and that's why the simplifier is breaking. TL;DR: there a shortcoming in Lint, which I'll fix. Beyond that, GHC should really give a better error than a Lint failure in this case, but it's a bit exotic, and I'm not really sure where the best place to do it is. Maybe `chekcValidType`? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15648#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler