[GHC] #13804: MonoLocalBinds/RankNTypes type inference regression in GHC 8.2

[GHC]

#13804: MonoLocalBinds/RankNTypes type inference regression in GHC 8.2
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.1-rc2
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by RyanGlScott:

@@ -122,1 +122,1 @@
- {{{#!hs
+ {{{

New description:

 I encountered this problem when trying to compile the `ivory-bsp-stm32`
 library (unsuccessfully) with GHC 8.2. Here's a somewhat minimized
 example:

 {{{#!hs
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE KindSignatures #-}
 -- Not enabling MonoLocalBinds makes it compile again
 {-# LANGUAGE MonoLocalBinds #-}
 {-# LANGUAGE RankNTypes #-}
 module Bug where

 import GHC.TypeLits

 i2cPeripheralDriver :: I2CPeriph
                     -> ChanOutput ('Stored ITime)
                     -> Monitor e ()
 i2cPeripheralDriver periph watchdog_per = do
   let sendresult' :: Ivory eff ()
       sendresult' = do
           -- Commenting out the line below makes it compile again
           clearSR1 periph

           return undefined
       sendresult = sendresult'

   handler watchdog_per undefined $ do
     callback $ \_ -> do
       sendresult

   return undefined

 clearSR1 :: I2CPeriph -> Ivory eff ()
 clearSR1 = undefined

 -----
 -- Auxiliary definitions
 -----

 data ITime
 data I2CPeriph = I2CPeriph

 data Ivory (eff :: Effects) a
 instance Functor (Ivory eff)
 instance Applicative (Ivory eff)
 instance Monad (Ivory eff)

 data Monitor e a
 instance Functor (Monitor e)
 instance Applicative (Monitor e)
 instance Monad (Monitor e)

 data ChanOutput (a :: Area *)

 data RefScope =
     Global
   | forall s. Stack s

 type ConstRef = Pointer 'Valid 'Const -- :: RefScope -> Area * -> *

 data Nullability = Nullable | Valid
 data Constancy = Const | Mutable

 data Pointer (n :: Nullability)
              (c :: Constancy)
              (s :: RefScope)
              (a :: Area *)

 type AllocEffects s =
   'Effects 'NoReturn 'NoBreak ('Scope s) -- :: Effects

 data Effects = Effects ReturnEff BreakEff AllocEff

 data ReturnEff =
     forall t. Returns t
   | NoReturn

 data BreakEff = Break | NoBreak

 data AllocEff =
     forall s. Scope s
   | NoAlloc

 callback ::
   (IvoryArea a,
    IvoryZero a) =>
   (forall (s :: RefScope) s'.
    ConstRef s a
    -> Ivory
         (AllocEffects s') ())
   -> Handler a e ()
 callback _ = undefined

 handler ::
   (IvoryArea a,
    IvoryZero a) =>
   ChanOutput a -> String -> Handler a e () -> Monitor e ()
 data Handler (area :: Area *) e a
 handler = undefined

 data Area k
   = Struct Symbol
   | Array Nat (Area k)
   | CArray (Area k)
   | Stored k

 data Time

 class IvoryArea (a :: Area *)
 class IvoryZero (area :: Area *) where
 class IvoryType t
 instance IvoryType ITime
 instance IvoryType a => IvoryArea ('Stored a)
 class IvoryZeroVal a
 instance IvoryZeroVal ITime
 instance IvoryZeroVal a => IvoryZero ('Stored a)
 }}}

 In GHC 7.10 and 8.0, this compiles. With GHC 8.2, however, it errors:

 {{{
 GHCi, version 8.2.0.20170522: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )

 Bug.hs:25:7: error:
     • Couldn't match type ‘eff0’ with ‘AllocEffects s'’
         because type variable ‘s'’ would escape its scope
       This (rigid, skolem) type variable is bound by
         a type expected by the context:
           forall (s :: RefScope) s'.
           ConstRef s ('Stored ITime) -> Ivory (AllocEffects s') ()
         at Bug.hs:(24,5)-(25,16)
       Expected type: Ivory (AllocEffects s') ()
         Actual type: Ivory eff0 ()
     • In a stmt of a 'do' block: sendresult
       In the expression: do sendresult
       In the second argument of ‘($)’, namely ‘\ _ -> do sendresult’
     • Relevant bindings include
         sendresult :: Ivory eff0 () (bound at Bug.hs:21:7)
    |
 25 |       sendresult
    |       ^^^^^^^^^^
 }}}

--

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13804#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler