#15589: Always promoting metavariables during type inference may be wrong -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Here's another idea, IMHO far better than "storing the list of variables in scope". * Give every `Implication` a unique identity. The already have one, in the form of the EvBindsVar (see `ebv_uniq`), but we should probably promote it to the `Implication` itself, replacing the `ic_tclvl` field. * Instead of a level, store in a (meta) TcTyVar the ''identity of its enclosing implication''. Call that the ''implication parent'' of the TcTyVar. * A `TcTyVar` is touchable iff its implication parent is the current implication. * Levels are already immutable; when promoting a tyvar we make a new one, and we can still do that fine. Implication identities completely replace level numbers. Now, in the example, we'll give `x` the type {{{ x :: forall a (b :: kappa[i34]) (d :: a). SameKind (IfK c b d) d plus the leftover implication constraint forall[i34] a b d. If cb kappa[i34] a ~ a }}} Here `i34` is the identity of the parent implication, which arises from the `forall` in the type signature. That implication constraint is emitted unsolved; and x's type is in the environment with this now-forever-untouchable `kappa[i34]`. It can only be touched (and hence solved) when we have another go at solving that implication constraint -- which we will. And Bob's your uncle. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15589#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler