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

11 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:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Actually, I'm not sure if I find this occurs check explanation entirely
 satisfactory. SkorikGG points out
 [https://github.com/ekmett/constraints/issues/55#issuecomment-300767277
 here] that you can make this program work with a slight tweak:

 {{{#!hs
 {-# 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?

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13674#comment:7
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler