[GHC] #9701: GADTs not specialized properly

[GHC]

#9701: GADTs not specialized properly
-------------------------------------+-------------------------------------
              Reporter:  dfeuer      |            Owner:
                  Type:  bug         |           Status:  new
              Priority:  normal      |        Milestone:
             Component:  Compiler    |          Version:  7.9
            Resolution:              |         Keywords:
      Operating System:              |     Architecture:  Unknown/Multiple
  Unknown/Multiple                   |       Difficulty:  Unknown
       Type of failure:  Runtime     |       Blocked By:
  performance bug                    |  Related Tickets:
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------

Comment (by dfeuer):

 Replying to [comment:3 ekmett]:
 > 3.) We actually '''have''' to take the "nearest" instance when you bind
 instances in local scope. Why? `ImplicitParams` unfortunately exist.
 >
 > If you have `(?x :: Int)` in scope
 >
 > and you come across `let ?x = 12 :: Int in ...` you need to switch to
 the new witness of `(?x :: Int)`.
 >
 > The same should work if you open a `Dict (?x :: Int)`.

 What am I missing here? Core distinguishes dictionaries that came from
 type classes from implicit parameters, doesn't it? If someone decides to
 implement some sort of local instance extension, as suggested by
 [http://okmij.org/ftp/Haskell/tr-15-04.pdf Oleg Kiselyov and Chung-chieh
 Shan], some restrictions are required to make anything work (as discussed
 in the paper). I believe the restrictions they describe would probably
 skirt the problem you consider, because (if my vague understanding is
 sufficiently correct) the types won't match where the dictionary
 replacement would be problematic.

 Also, I realized today that things can be simplified some more, and
 perhaps in a way you might find more convincing:

 {{{#!hs
 data Silly a where
   Silly :: Num a => a -> Silly a

 potato :: Int -> Silly Int -> Int
 potato x (Silly _) = x + x
 }}}

 Even here, `potato` uses the dictionary it takes from `Silly`. If there
 were incoherent instances in the air, this would not really be a result to
 be proud of.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9701#comment:9>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler