[GHC] #13555: Typechecker regression when combining PolyKinds and MonoLocalBinds

9 Apr 2017

      #13555: Typechecker regression when combining PolyKinds and MonoLocalBinds
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  highest        |         Milestone:  8.2.1
          Component:  Compiler       |           Version:  8.1
  (Type checker)                     |
           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:
-------------------------------------+-------------------------------------
 `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:

 {{{#!hs
 {-# 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.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13555
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler