Opened 2 months ago

Closed 2 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 RyanGlScott)

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 2 months ago by RyanGlScott

Summary: GHC doesn't discharge heterogenous equality constraint when it ought toGHC doesn't discharge heterogeneous equality constraint when it ought to

comment:2 Changed 2 months ago by oerjan

For what it's worth, it still doesn't help (in GHC 8.0.1) if I change all the ~s to ~~s.

comment:3 Changed 2 months ago by oerjan

Cc: oerjan added

comment:4 Changed 2 months ago by RyanGlScott

Description: modified (diff)

comment:5 Changed 2 months ago by goldfire

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 2 months ago by RyanGlScott

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 2 months ago by RyanGlScott

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 2 months ago by oerjan

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 2 months ago by goldfire

comment:8 is essentially correct. Consider two scenarios:

  1. We have a Given proving blah and a Wanted blah. We use the Given to solve the Wanted. Later, we learn that blah is Lcm m m ~ m, but nothing above changes.
  1. We have a Given proving blah. We learn that blah is Lcm m m ~ m, so we mark it as insoluble. Then, we get a Wanted blah, which we see is Lcm 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 2 months ago by RyanGlScott

Summary: GHC doesn't discharge heterogeneous equality constraint when it ought toPoor 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:11 Changed 2 months ago by Simon Peyton Jones <simonpj@…>

In c2eea08/ghc:

Make isInsolubleOccursCheck more aggressive

Consider
  type family F a :: * -> *

Then (a ~ F Int a) is an insoluble occurs check, and can be reported
as such.  Previous to this patch, TcType.isInsolubleOccursCheck was
treating any type-family application (including an over-saturated one)
as unconditionally not-insoluble.

This really only affects error messages, and then only slightly. I
tripped over this when investigating  Trac #13674.

comment:12 Changed 2 months ago by Simon Peyton Jones <simonpj@…>

In 8dc6d645/ghc:

Re-engineer Given flatten-skolems

The big change here is to fix an outright bug in flattening of Givens,
albeit one that is very hard to exhibit.  Suppose we have the constraint
    forall a. (a ~ F b) => ..., (forall c. ....(F b)...) ...

Then
 - we'll flatten the (F) b to a fsk, say  (F b ~ fsk1)
 - we'll rewrite the (F b) inside the inner implication to 'fsk1'
 - when we leave the outer constraint we are suppose to unflatten;
   but that fsk1 will still be there
 - if we re-simplify the entire outer implication, we'll re-flatten
   the Given (F b) to, say, (F b ~ fsk2)
Now we have two fsks standing for the same thing, and that is very
wrong.

Solution: make fsks behave more like fmvs:
 - A flatten-skolem is now a MetaTyVar, whose MetaInfo is FlatSkolTv
 - We "fill in" that meta-tyvar when leaving the implication
 - The old FlatSkol form of TcTyVarDetails is gone completely
 - We track the flatten-skolems for the current implication in
   a new field of InertSet, inert_fsks.

See Note [The flattening story] in TcFlatten.

In doing this I found various other things to fix:

* I removed the zonkSimples from TcFlatten.unflattenWanteds; it wasn't
  needed.   But I added one in TcSimplify.floatEqualities, which does
  the zonk precisely when it is needed.

* Trac #13674 showed up a case where we had
     - an insoluble Given,   e.g.  a ~ [a]
     - the same insoluble Wanted   a ~ [a]
  We don't use the Given to rewwrite the Wanted (obviously), but
  we therefore ended up reporting
      Can't deduce (a ~ [a]) from (a ~ [a])
  which is silly.

  Conclusion: when reporting errors, make the occurs check "win"
  See Note [Occurs check wins] in TcErrors

comment:13 Changed 2 months ago by simonpj

Resolution: fixed
Status: newclosed
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).

Note: See TracTickets for help on using tickets.