#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 AlejandroSerrano): Indeed, when working in the ''Guarded impredicativity'' paper we considered delaying instantiations as a solution, which we rejected because it was quite complicated. Applying that solution to this case, the instantiation of {{{ x :: forall (a :: Type) (b :: kappa[i34]) (d :: a). <stuff> }}} would be forbidden until `kappa[i34]` is known. That entails that `d` is not instantiated either, as it appears later in the time. However, in the paper we do not explicitly mention kind signatures. We assume that if we have a quantified type, we can always instantiate its variables -- we only have to choose whether we instantiate them with some restrictions or not. There is some work to be done to ensure that this kind of scenarios doesn't break the invariants for termination of checking. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15589#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler