[GHC] #13674: GHC doesn't discharge heterogenous equality constraint when it ought to
GHC
ghc-devs at haskell.org
Tue May 9 19:24:29 UTC 2017
#13674: GHC doesn't discharge heterogenous equality constraint when it ought to
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 8.0.1
(Type checker) |
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:
-------------------------------------+-------------------------------------
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
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:54: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:53: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: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)
| ^^^^^^^
Bug.hs:54: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: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
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: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)
| ^^^^^^^
}}}
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/8.2.1/bin/ghci Bug.hs -fprint-explicit-kinds
GHCi, version 8.2.0.20170505: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:54: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:53: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: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)
| ^^^^^^^
Bug.hs:54: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: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
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: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)
| ^^^^^^^
}}}
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>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list