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

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