[GHC] #13674: GHC doesn't discharge heterogeneous equality constraint when it ought to
GHC
ghc-devs at haskell.org
Wed May 10 14:07:16 UTC 2017
#13674: GHC doesn't discharge heterogeneous equality constraint when it ought to
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type | Version: 8.0.1
checker) |
Resolution: | Keywords: TypeInType
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: |
-------------------------------------+-------------------------------------
Description changed by RyanGlScott:
@@ -51,0 +51,9 @@
+ instance KnownNat n => Num (GF n) where
+ xf@(GF x) + GF y = GF $ (x+y) `mod` (natVal xf)
+ xf@(GF x) - GF y = GF $ (x-y) `mod` (natVal xf)
+ xf@(GF x) * GF y = GF $ (x*y) `mod` (natVal xf)
+ abs = id
+ signum xf@(GF x) | x==0 = xf
+ | otherwise = GF 1
+ fromInteger = GF
+
@@ -74,1 +83,1 @@
- Bug.hs:54:21: error:
+ Bug.hs:63:21: error:
@@ -79,1 +88,1 @@
- at Bug.hs:53:1-44
+ at Bug.hs:62:1-44
@@ -90,5 +99,5 @@
- y :: GF m (bound at Bug.hs:54:17)
- x :: GF m (bound at Bug.hs:54:6)
- bar :: GF m -> GF m -> GF m (bound at Bug.hs:54:1)
- |
- 54 | bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @()
+ y :: GF m (bound at Bug.hs:63:17)
+ x :: GF m (bound at Bug.hs:63:6)
+ bar :: GF m -> GF m -> GF m (bound at Bug.hs:63:1)
+ |
+ 63 | bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @()
@@ -98,1 +107,1 @@
- Bug.hs:54:31: error:
+ Bug.hs:63:31: error:
@@ -103,5 +112,5 @@
- at Bug.hs:54:31-85
- ‘m’ is a rigid type variable bound by
- the type signature for:
- bar :: forall (m :: Nat). KnownNat m => GF m -> GF m -> GF m
- at Bug.hs:53:1-44
+ at Bug.hs:63:31-85
+ ‘m’ is a rigid type variable bound by
+ the type signature for:
+ bar :: forall (m :: Nat). KnownNat m => GF m -> GF m -> GF m
+ at Bug.hs:62:1-44
@@ -115,5 +124,5 @@
- y :: GF m (bound at Bug.hs:54:17)
- x :: GF m (bound at Bug.hs:54:6)
- bar :: GF m -> GF m -> GF m (bound at Bug.hs:54:1)
- |
- 54 | bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @()
+ y :: GF m (bound at Bug.hs:63:17)
+ x :: GF m (bound at Bug.hs:63:6)
+ bar :: GF m -> GF m -> GF m (bound at Bug.hs:63:1)
+ |
+ 63 | bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @()
@@ -136,2 +145,2 @@
- $ /opt/ghc/8.2.1/bin/ghci Bug.hs -fprint-explicit-kinds
- GHCi, version 8.2.0.20170505: http://www.haskell.org/ghc/ :? for help
+ $ /opt/ghc/head/bin/ghci Bug.hs -fprint-explicit-kinds
+ GHCi, version 8.3.20170509: http://www.haskell.org/ghc/ :? for help
@@ -141,1 +150,1 @@
- Bug.hs:54:21: error:
+ Bug.hs:63:21: error:
@@ -146,1 +155,1 @@
- at Bug.hs:53:1-44
+ at Bug.hs:62:1-44
@@ -157,5 +166,5 @@
- y :: GF m (bound at Bug.hs:54:17)
- x :: GF m (bound at Bug.hs:54:6)
- bar :: GF m -> GF m -> GF m (bound at Bug.hs:54:1)
- |
- 54 | bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @()
+ y :: GF m (bound at Bug.hs:63:17)
+ x :: GF m (bound at Bug.hs:63:6)
+ bar :: GF m -> GF m -> GF m (bound at Bug.hs:63:1)
+ |
+ 63 | bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @()
@@ -165,1 +174,1 @@
- Bug.hs:54:31: error:
+ Bug.hs:63:31: error:
@@ -170,5 +179,5 @@
- at Bug.hs:54:31-85
- ‘m’ is a rigid type variable bound by
- the type signature for:
- bar :: forall (m :: Nat). KnownNat m => GF m -> GF m -> GF m
- at Bug.hs:53:1-44
+ at Bug.hs:63:31-85
+ ‘m’ is a rigid type variable bound by
+ the type signature for:
+ bar :: forall (m :: Nat). KnownNat m => GF m -> GF m -> GF m
+ at Bug.hs:62:1-44
@@ -182,7 +191,7 @@
- y :: GF m (bound at Bug.hs:54:17)
- x :: GF m (bound at Bug.hs:54:6)
- bar :: GF m -> GF m -> GF m (bound at Bug.hs:54:1)
- |
- 54 | bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @()
- (lcmIsIdempotent @m)
- | ^^^^^^^
+ y :: GF m (bound at Bug.hs:63:17)
+ x :: GF m (bound at Bug.hs:63:6)
+ bar :: GF m -> GF m -> GF m (bound at Bug.hs:63:1)
+ |
+ 63 | bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @()
+ (lcmIsIdempotent @m)
+ |
New description:
Here's some code, reduced from an example in
https://github.com/ekmett/constraints/issues/55:
{{{#!hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
import Data.Proxy
import GHC.Exts (Constraint)
import GHC.TypeLits
import Unsafe.Coerce (unsafeCoerce)
data Dict :: Constraint -> * where
Dict :: a => Dict a
infixr 9 :-
newtype a :- b = Sub (a => Dict b)
-- | Given that @a :- b@, derive something that needs a context @b@, using
the context @a@
(\\) :: a => (b => r) -> (a :- b) -> r
r \\ Sub Dict = r
newtype Magic n = Magic (KnownNat n => Dict (KnownNat n))
magic :: forall n m o. (Integer -> Integer -> Integer) -> (KnownNat n,
KnownNat m) :- KnownNat o
magic f = Sub $ unsafeCoerce (Magic Dict) (natVal (Proxy :: Proxy n) `f`
natVal (Proxy :: Proxy m))
type family Lcm :: Nat -> Nat -> Nat where
axiom :: forall a b. Dict (a ~ b)
axiom = unsafeCoerce (Dict :: Dict (a ~ a))
lcmNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Lcm n m)
lcmNat = magic lcm
lcmIsIdempotent :: forall n. Dict (n ~ Lcm n n)
lcmIsIdempotent = axiom
newtype GF (n :: Nat) = GF Integer
instance KnownNat n => Num (GF n) where
xf@(GF x) + GF y = GF $ (x+y) `mod` (natVal xf)
xf@(GF x) - GF y = GF $ (x-y) `mod` (natVal xf)
xf@(GF x) * GF y = GF $ (x*y) `mod` (natVal xf)
abs = id
signum xf@(GF x) | x==0 = xf
| otherwise = GF 1
fromInteger = GF
x :: GF 5
x = GF 3
y :: GF 5
y = GF 4
foo :: (KnownNat m, KnownNat n) => GF m -> GF n -> GF (Lcm m n)
foo m@(GF x) n@(GF y) = GF $ (x*y) `mod` (lcm (natVal m) (natVal n))
bar :: (KnownNat m) => GF m -> GF m -> GF m
bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @()
(lcmIsIdempotent @m)
}}}
Compiling this (with either GHC 8.0.1, 8.0.2, 8.2.1, or HEAD) gives you a
downright puzzling type error:
{{{
$ /opt/ghc/head/bin/ghci Bug.hs
GHCi, version 8.3.20170509: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:63:21: error:
• Couldn't match type ‘m’ with ‘Lcm m m’
‘m’ is a rigid type variable bound by
the type signature for:
bar :: forall (m :: Nat). KnownNat m => GF m -> GF m -> GF m
at Bug.hs:62:1-44
Expected type: GF m
Actual type: GF (Lcm m m)
• In the first argument of ‘(-)’, namely ‘foo x y’
In the expression:
foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
In an equation for ‘bar’:
bar (x :: GF m) y
= foo x y - foo y x \\ lcmNat @m @m \\ Sub @()
(lcmIsIdempotent @m)
• Relevant bindings include
y :: GF m (bound at Bug.hs:63:17)
x :: GF m (bound at Bug.hs:63:6)
bar :: GF m -> GF m -> GF m (bound at Bug.hs:63:1)
|
63 | bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @()
(lcmIsIdempotent @m)
| ^^^^^^^
Bug.hs:63:31: error:
• Could not deduce: m ~ Lcm m m
from the context: m ~ Lcm m m
bound by a type expected by the context:
m ~ Lcm m m => GF m
at Bug.hs:63:31-85
‘m’ is a rigid type variable bound by
the type signature for:
bar :: forall (m :: Nat). KnownNat m => GF m -> GF m -> GF m
at Bug.hs:62:1-44
Expected type: GF m
Actual type: GF (Lcm m m)
• In the first argument of ‘(\\)’, namely ‘foo y x’
In the first argument of ‘(\\)’, namely ‘foo y x \\ lcmNat @m @m’
In the second argument of ‘(-)’, namely
‘foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)’
• Relevant bindings include
y :: GF m (bound at Bug.hs:63:17)
x :: GF m (bound at Bug.hs:63:6)
bar :: GF m -> GF m -> GF m (bound at Bug.hs:63:1)
|
63 | bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @()
(lcmIsIdempotent @m)
| ^^^^^^^
}}}
In particular, I'd like to emphasize this part:
{{{
• Could not deduce: m ~ Lcm m m
from the context: m ~ Lcm m m
}}}
Wat!? Surely, GHC can deduce `m ~ Lcm m m` from `m ~ Lcm m m`? I decided
to flip on `-fprint-explicit-kinds` and see if there was some other issue
lurking beneath the surface:
{{{
$ /opt/ghc/head/bin/ghci Bug.hs -fprint-explicit-kinds
GHCi, version 8.3.20170509: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:63:21: error:
• Couldn't match type ‘m’ with ‘Lcm m m’
‘m’ is a rigid type variable bound by
the type signature for:
bar :: forall (m :: Nat). KnownNat m => GF m -> GF m -> GF m
at Bug.hs:62:1-44
Expected type: GF m
Actual type: GF (Lcm m m)
• In the first argument of ‘(-)’, namely ‘foo x y’
In the expression:
foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
In an equation for ‘bar’:
bar (x :: GF m) y
= foo x y - foo y x \\ lcmNat @m @m \\ Sub @()
(lcmIsIdempotent @m)
• Relevant bindings include
y :: GF m (bound at Bug.hs:63:17)
x :: GF m (bound at Bug.hs:63:6)
bar :: GF m -> GF m -> GF m (bound at Bug.hs:63:1)
|
63 | bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @()
(lcmIsIdempotent @m)
| ^^^^^^^
Bug.hs:63:31: error:
• Could not deduce: (m :: Nat) ~~ (Lcm m m :: Nat)
from the context: m ~ Lcm m m
bound by a type expected by the context:
m ~ Lcm m m => GF m
at Bug.hs:63:31-85
‘m’ is a rigid type variable bound by
the type signature for:
bar :: forall (m :: Nat). KnownNat m => GF m -> GF m -> GF m
at Bug.hs:62:1-44
Expected type: GF m
Actual type: GF (Lcm m m)
• In the first argument of ‘(\\)’, namely ‘foo y x’
In the first argument of ‘(\\)’, namely ‘foo y x \\ lcmNat @m @m’
In the second argument of ‘(-)’, namely
‘foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)’
• Relevant bindings include
y :: GF m (bound at Bug.hs:63:17)
x :: GF m (bound at Bug.hs:63:6)
bar :: GF m -> GF m -> GF m (bound at Bug.hs:63:1)
|
63 | bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @()
(lcmIsIdempotent @m)
|
}}}
Well, not a whole lot changed. We now have this, slightly more specific
error instead:
{{{
• Could not deduce: (m :: Nat) ~~ (Lcm m m :: Nat)
from the context: m ~ Lcm m m
}}}
Huh, this is flummoxing. Surely `(m :: Nat) ~~ (Lcm m m :: Nat)` ought to
be the same thing as `m ~ Lcm m m`, right?
--
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13674#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list