Skip to content

MonoLocalBinds/RankNTypes type inference regression in GHC 8.2

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

{-# 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
   |       ^^^^^^^^^^
Edited by Ryan Scott
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information