#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 simonpj):
there might be a variable born as a skolem that nevertheless mentions unification variables in its kind.
Rats. Yes, that is true. Also an exisential match on {{{ data T k where MkT :: forall (a :: k). blah -> T k }}}
"forbid lexical meta-tyvars in type signatures" but that's a huge hammer.
Yes, that is what I'm saying. Let's review the problem: * We can't instantiate a type signature that contains a meta-variable if that meta-variable might later be instantiated to one of the quantified variables of the signature. (Unless we venture in the uncharted waters of delayed substitutions.) * If we have solved all the constraints arising from the signature, and any free meta-variables are from an outer level, there is no problem -- outer-level variables can't be solved in a way that mentions the inner quantifiers. * But "solving all the constraints" might (in obscure cases) depend on whether or not we have worked out the value of some outer level variable. Thus `If alpha[0] beta[1] Int ~ a[1]`; if `alpha` turns out to be `True` we learn that `beta := a`. * We could reject the obscure situation, but we can't detect when it happens: suppose we unified `alpha := True` much much earlier and zonked it away. * This kind of order-dependence already arises when we use `simplifyInfer` in `NoMonoLocalBinds`; here again, an outer `alpha[0]` might unlock an inner constraint. But with `MonoLocalBinds` (our well-behaved case), it does not happen. We'd like a `MonoLocalBinds` for type signatures, which ensures their good behaviour. But I don't see one, apart from the big hammer of saying that the type can mention only lexically scoped variables whose type and kind are fixed from the moment it comes into scope. (And even that is not a very well-defined statement.) It's very frustrating that there is no simple way to identify a well- behaved subset. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15589#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler