Typechecker regression when combining PolyKinds and MonoLocalBinds

lol-0.6.0.0 from Hackage currently fails to build with GHC 8.2.1 because of this regression. Here is a minimized example:

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
module Crypto.Lol.Types.FiniteField (GF(..)) where

import Data.Functor.Identity (Identity(..))

data T a
type Polynomial a = T a
newtype GF fp d = GF (Polynomial fp)
type CRTInfo r = (Int -> r, r)
type Tagged s b = TaggedT s Identity b
newtype TaggedT s m b = TagT { untagT :: m b }

class Reflects a i where
  value :: Tagged a i

class CRTrans mon r where
  crtInfo :: Reflects m Int => TaggedT m mon (CRTInfo r)

instance CRTrans Maybe (GF fp d) where
  crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))
  crtInfo = undefined

This typechecks OK with GHC 8.0.2, but with 8.2.1, it complains:

$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.0.20170403: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Crypto.Lol.Types.FiniteField ( Bug.hs, interpreted )

Bug.hs:25:14: error:
    • Couldn't match type ‘k0’ with ‘k2’
        because type variable ‘k2’ would escape its scope
      This (rigid, skolem) type variable is bound by
        the type signature for:
          crtInfo :: forall k2 (m :: k2).
                     Reflects m Int =>
                     TaggedT m Maybe (CRTInfo (GF fp d))
        at Bug.hs:25:14-79
      Expected type: TaggedT m Maybe (CRTInfo (GF fp d))
        Actual type: TaggedT m Maybe (CRTInfo (GF fp d))
    • When checking that instance signature for ‘crtInfo’
        is more general than its signature in the class
        Instance sig: forall (m :: k0).
                      Reflects m Int =>
                      TaggedT m Maybe (CRTInfo (GF fp d))
           Class sig: forall k2 (m :: k2).
                      Reflects m Int =>
                      TaggedT m Maybe (CRTInfo (GF fp d))
      In the instance declaration for ‘CRTrans Maybe (GF fp d)’
   |
25 |   crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))
   |              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Bug.hs:25:14: error:
    • Could not deduce (Reflects m Int)
      from the context: Reflects m Int
        bound by the type signature for:
                   crtInfo :: forall k2 (m :: k2).
                              Reflects m Int =>
                              TaggedT m Maybe (CRTInfo (GF fp d))
        at Bug.hs:25:14-79
      The type variable ‘k0’ is ambiguous
    • When checking that instance signature for ‘crtInfo’
        is more general than its signature in the class
        Instance sig: forall (m :: k0).
                      Reflects m Int =>
                      TaggedT m Maybe (CRTInfo (GF fp d))
           Class sig: forall k2 (m :: k2).
                      Reflects m Int =>
                      TaggedT m Maybe (CRTInfo (GF fp d))
      In the instance declaration for ‘CRTrans Maybe (GF fp d)’
   |
25 |   crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))
   |              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Notably, both PolyKinds and MonoLocalBinds are required to trigger this bug.

Trac metadata

Trac field	Value
Version	8.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	highest
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture