#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: TypeInType 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 goldfire): But how do we instantiate the type of `x` at an occurrence? We'll generate `alpha`, `beta`, and `delta` to instantiate for `a`, `b`, and `d`, respectively. We figured out a while ago that `a`'s kind -- hence `alpha`'s -- is `Type`. But what will `beta`'s kind be? It can't quite be `kappa[i34]`, because `kappa[i34]` might turn out to mention `a`, not `alpha`. Instead, it has to be `kappa[i34][a |-> alpha]`, as some kind of suspended substitution. My thesis (and Adam's) does this by including a list of variables at every occurrence of a unification variable. Thus, it would be `beta_[alpha]`, where it's understood that `alpha` is the instantiation of variables that might appear in `beta`'s kind. Similarly, `delta` would really be `delta_[alpha,beta]`, because `delta` is preceded by two instantiated variables. Really, all comment:1 does is to come up with a concise (and very convenient) way to store lists of variables, by naming the lists and storing the names. But I don't think it eliminates all the attendant complication of instantiation. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15589#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler