#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 (13)
comment:1 Changed 18 months ago by
Cc: | goldfire added |
---|
comment:2 Changed 18 months ago by
This smells very much like a dup of #13549, which I've not had more time to examine. Perhaps tomorrow.
comment:3 Changed 18 months ago by
Keywords: | TypeInType added |
---|
comment:4 Changed 18 months ago by
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 SigTv
s. 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
- Advertise this as a user-facing change (a bug-fix, really) and tell users to add kind signatures, or
- Avoid the new logic with
-XNoTypeInType
.
I prefer (1) because it's simpler, but not strongly.
comment:5 Changed 18 months ago by
To be clear, when you say "add a kind signature", where in the above program should you add a kind signature?
comment:6 Changed 18 months ago by
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 18 months ago by
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 17 months ago by
Priority: | highest → high |
---|
comment:9 Changed 17 months ago by
Differential Rev(s): | → Phab:D3472 |
---|---|
Status: | new → patch |
I took a shot at option (1) (documenting the current behavior as correct) in Phab:D3472.
comment:11 Changed 17 months ago by
Status: | patch → merge |
---|
I added a section about this behavior in the GHC 8.2 migration guide.
comment:12 Changed 17 months ago by
Resolution: | → fixed |
---|---|
Status: | merge → closed |
Merged with 3b4af97b77a0ca21a29cc9829ccfab6871be035f.
comment:13 Changed 7 weeks ago by
Note that as a result of commit c955a514f033a12f6d0ab0fbacec3e18a5757ab5 (Remove decideKindGeneralisationPlan
), the original program now typechecks again.
Commit 109a2429493c2a2d5481b67f5b0c1086a959813e caused this.
Is this perhaps related to #13549?