Re: [GHC] #13674: GHC doesn't discharge heterogeneous equality constraint when it ought to

10 May 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

    