Opened 5 months ago
Closed 4 months ago
#13674 closed bug (fixed)
Poor error message which masks occurs-check failure
Reported by: | RyanGlScott | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler (Type checker) | Version: | 8.0.1 |
Keywords: | TypeInType | Cc: | oerjan |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Test Case: | indexed_types/should_fail/T13674 |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description (last modified by )
Here's some code, reduced from an example in https://github.com/ekmett/constraints/issues/55:
{-# 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?
Change History (13)
comment:1 Changed 5 months ago by
Summary: | GHC doesn't discharge heterogenous equality constraint when it ought to → GHC doesn't discharge heterogeneous equality constraint when it ought to |
---|
comment:2 Changed 5 months ago by
comment:3 Changed 5 months ago by
Cc: | oerjan added |
---|
comment:4 Changed 5 months ago by
Description: | modified (diff) |
---|
comment:5 Changed 5 months ago by
The original program is wrong, but the error message also is wrong. Because Lcm
is a nullary type family, the constraint m ~ Lcm m m
is morally equivalent to m ~ Either m m
. This constraint is an occurs-check failure and is surely going to lead to an error. It seems that the error-reporting code is mischaracterizing it, though.
comment:6 Changed 5 months ago by
This constraint is an occurs-check failure and is surely going to lead to an error.
Ah, that's a good point. I forgot that Lcm m m
doesn't reduce as a type family (you're only ever to get out the lcm
of m
and m
at the value level by using knownNat
with the reflection-style trickery in magic
, but this doesn't work at the type level).
comment:7 Changed 5 months ago by
Actually, I'm not sure if I find this occurs check explanation entirely satisfactory. SkorikGG points out here that you can make this program work with a slight tweak:
{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} import Data.Proxy import Data.Type.Equality 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 (Lcm n 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)) dictToRefl :: Dict (a ~ b) -> a :~: b dictToRefl Dict = Refl bar :: (KnownNat m) => GF m -> GF m -> GF m bar (x :: GF m) y = castWith (apply Refl $ dictToRefl (lcmIsIdempotent :: Dict (Lcm m m ~ m))) (foo x y - foo y x) \\ lcmNat @m @m z :: GF 5 z = bar x y
Notice that in bar
, we're using a trick of converting the lcmIsIdempotent
Dict
to a (:~:)
using dictToRefl
. And it's clear that we are using the fact that Lcm m m ~ m
in order for bar
to typecheck, but this time, GHC accepts it! Should it?
comment:8 Changed 5 months ago by
I assume the difference, as usual in these kinds of tricks, is that in the workaround, GHC never gets directly asked to produce Lcm m m ~ m
as a wanted constraint, and so never gets a chance to smell anything fishy.
comment:9 Changed 5 months ago by
comment:8 is essentially correct. Consider two scenarios:
- We have a Given proving
blah
and a Wantedblah
. We use the Given to solve the Wanted. Later, we learn thatblah
isLcm m m ~ m
, but nothing above changes.
- We have a Given proving
blah
. We learn thatblah
isLcm m m ~ m
, so we mark it as insoluble. Then, we get a Wantedblah
, which we see isLcm m m ~ m
. This, too, is marked as insoluble.
In case 1, we'll succeed; in case 2, we'll fail. The problem is that the only difference in these cases is the order in which constraints are treated and/or solved, something notoriously difficult to control. The "fix" for this problem is not to error on occurs-checks, which would then allow us to succeed in case 2. That seems unsatisfactory, though, because even if occurs-checks don't immediately error, we'll have a hard time solving m ~ Lcm m m
from Lcm m m ~ m
.
I'm inclined to say that we let this behavior stand. Note that when we accept the program, nothing goes wrong.
comment:10 Changed 5 months ago by
Summary: | GHC doesn't discharge heterogeneous equality constraint when it ought to → Poor error message which masks occurs-check failure |
---|
I'm inclined to say that we let this behavior stand. Note that when we accept the program, nothing goes wrong.
OK, I can live with that. Sorry for derailing the discussion in the ticket a bit, but I wanted make sure I understood what was going on.
Since the behavior here seems to be correct (modulo error messages), I'll change the title accordingly.
comment:13 Changed 4 months ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
Test Case: | → indexed_types/should_fail/T13674 |
This was a very interesting ticket that showed up quite a deep bug. Thanks!
I don't think this is worth merging. It's a very dark corner, the change is significant, and there's a chance that I've done something wrong (notwithstanding validate).
For what it's worth, it still doesn't help (in GHC 8.0.1) if I change all the
~
s to~~
s.