#13959: substTyVar's definition is highly dubious -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D3732 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Just to add: Rule (+) means that the following program is illegal: {{{ forall (k:*). forall (a:k). forall (k:*->*). a }}} Note the shadowing: there are really two k's. It's illegal according to (+) because bringing the inner `k` into scope makes `a` (as well as the outer `k`) fall out of scope, because `a`'s kind mentions `k`. Why this rule? Because in the implementation we have kinds on every variable occurrence, and the kind on an occurrence should match that on the binder. So {{{ forall (a:*). (a:*) -> Int }}} is fine, but {{{ forall (a:*). T (a:*->*) }}} is not, because the kind on `a`'s occurrence doesn't match that at its binding site. And Rule (+) makes this illegal too: {{{ forall (k:*). forall (a:k). forall (k:*->*). (a:k) }}} because the kind at `a`'s occurrence is a different `k` to that at its binding site. Another way to say it is that `typeKind` (and `exprType`) yield sane results. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13959#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler