Opened 6 months ago

Closed 5 months ago

Last modified 5 months ago

#13555 closed bug (fixed)

Typechecker regression when combining PolyKinds and MonoLocalBinds

Reported by: RyanGlScott Owned by:
Priority: high Milestone: 8.2.1
Component: Compiler (Type checker) Version: 8.1
Keywords: TypeInType Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D3472
Wiki Page:

Description

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.

Change History (12)

comment:1 Changed 6 months ago by RyanGlScott

Cc: goldfire added

Commit 109a2429493c2a2d5481b67f5b0c1086a959813e caused this.

Is this perhaps related to #13549?

comment:2 Changed 6 months ago by goldfire

This smells very much like a dup of #13549, which I've not had more time to examine. Perhaps tomorrow.

comment:3 Changed 6 months ago by simonpj

Keywords: TypeInType added

comment:4 Changed 6 months ago by goldfire

I've figured this out. The new behavior is correct; the old behavior was a bug.

This is all to do with "let should not be generalized". With TypeInType, I extended that notion to the type level, saying that MonoLocalBinds implies that we should not perform kind generalization on type signatures that capture outer scoped type variables. This is the right behavior for precisely the same reasons it is at the term level: with local equalities on kinds and kind families, it's impossible to know how to generalize reliably.

In GHC 8.0, the check for in-scope type variables was subtly wrong and missed unified SigTvs. The new check is correct, as far as I can tell.

What's annoying here for users is that this a regression from 7.10, where MonoLocalBinds did not affect kind generalization. The good news is that the fix -- add a kind signature -- is fully backward-compatible. So, we could do either

  1. Advertise this as a user-facing change (a bug-fix, really) and tell users to add kind signatures, or
  1. Avoid the new logic with -XNoTypeInType.

I prefer (1) because it's simpler, but not strongly.

comment:5 Changed 6 months ago by RyanGlScott

To be clear, when you say "add a kind signature", where in the above program should you add a kind signature?

comment:6 Changed 6 months ago by RyanGlScott

Ah, I suppose you mean in the instance signature:

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

i.e., changing forall m to forall (m :: k).

comment:7 Changed 6 months ago by simonpj

I'd be happy with (1): let's add a user-manual section about kind generalisation, including saying when it does not happen.

Who will do that; Richard?

Also, is it enough to say

  crtInfo :: forall (m :: k) . (Reflects m Int) => ...blah...

or do we need

  crtInfo :: forall k (m :: k) . (Reflects m Int) => ...blah...

I think the former is ok, but is there a rule in the user manual that makes that clear?

comment:8 Changed 5 months ago by bgamari

Priority: highesthigh

comment:9 Changed 5 months ago by RyanGlScott

Differential Rev(s): Phab:D3472
Status: newpatch

I took a shot at option (1) (documenting the current behavior as correct) in Phab:D3472.

comment:10 Changed 5 months ago by Ben Gamari <ben@…>

In 18c3a7e/ghc:

Document the kind generalization behavior observed in #13555

The conclusion of #13555 was that a program which began to fail to
typecheck (starting in GHC 8.2) was never correct to begin with. Let's
document why this is the case with respect to `MonoLocalBinds`'
interaction with kind generalization. Also adds the reported program as
a `compile_fail` testcase.

Test Plan: make test TEST=T13555 # Also, read the docs

Reviewers: goldfire, simonpj, austin, bgamari

Reviewed By: goldfire, simonpj, bgamari

Subscribers: rwbarton, thomie

GHC Trac Issues: #13555

Differential Revision: https://phabricator.haskell.org/D3472

comment:11 Changed 5 months ago by RyanGlScott

Status: patchmerge

I added a section about this behavior in the GHC 8.2 migration guide.

comment:12 Changed 5 months ago by bgamari

Resolution: fixed
Status: mergeclosed
Last edited 5 months ago by bgamari (previous) (diff)
Note: See TracTickets for help on using tickets.