[GHC] #15589: Always promoting metavariables during type inference may be wrong

[GHC]

#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