Re: [GHC] #11715: Constraint vs *

19 Aug 2016

      #11715: Constraint vs *
-------------------------------------+-------------------------------------
        Reporter:  bgamari           |                Owner:
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.2.1
       Component:  Compiler (Type    |              Version:  8.0.1-rc1
  checker)                           |
      Resolution:                    |             Keywords:  Typeable
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by int-index):

 Here's a GHCi session you might find interesting. GHC just picks the first
 instance.

 {{{
 GHCi, version 8.1.20160813: http://www.haskell.org/ghc/  :? for help
 Prelude> :set -XGADTs
 Prelude> :set -XFlexibleContexts
 Prelude> data X where X :: Given Int => X
 Prelude> import Data.Reflection
 Prelude Data.Reflection> data X where X :: Given Int => X
 Prelude Data.Reflection> f X X = given :: Int
 Prelude Data.Reflection> a = give (10 :: Int) X
 Prelude Data.Reflection> b = give (20 :: Int) X
 Prelude Data.Reflection> f a b
 10
 Prelude Data.Reflection> f b a
 20
 }}}

 And here's the behavior of the type family example (when rewritten using
 reflection):

 {{{
 {-# LANGUAGE TypeFamilies, RankNTypes #-}

 import Data.Reflection

 type family F a where
   F Int = Int
   F a   = Char

 foo :: F a -> a -> (Given a => r) -> r
 foo x y k = give x $ give y $ k
 }}}

 {{{
 GHCi, version 8.1.20160813: http://www.haskell.org/ghc/  :? for help
 Prelude> :l With.hs
 [1 of 1] Compiling Main             ( With.hs, interpreted )
 Ok, modules loaded: Main.
 *Main> foo (10 :: Int) (20 :: Int) (given :: Int)
 20
 }}}

 If you specialize `foo` by adding `a ~ Int` to its type signature, you get
 a different result!

 {{{
 foo :: (a ~ Int) => F a -> a -> (Given a => r) -> r
 foo x y k = give x $ give y $ k
 }}}

 {{{
 *Main> foo (10 :: Int) (20 :: Int) (given :: Int)
 10
 }}}

 So, I say that the safe bet would be to *preserve* the current behavior,
 just get rid of `Given`. When multiple `with` are used, it is
 implementation defined which instance will get picked. Adding an equality
 constraint can indeed change the meaning of your code.

 But this is already the case, so at least we're not making things worse.

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