[GHC] #10226: Regression in constraint solver from 7.8 to 7.10

1 Apr 2015


      #10226: Regression in constraint solver from 7.8 to 7.10
-------------------------------------+-------------------------------------
              Reporter:  edsko       |             Owner:
                  Type:  bug         |            Status:  new
              Priority:  normal      |         Milestone:
             Component:  Compiler    |           Version:  7.10.1
  (Type checker)                     |  Operating System:  Unknown/Multiple
              Keywords:              |   Type of failure:  None/Unknown
          Architecture:              |        Blocked By:
  Unknown/Multiple                   |   Related Tickets:
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------
 Best explained by example:

 {{{#!hs
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE AllowAmbiguousTypes #-} -- only necessary in 7.10
 {-# LANGUAGE FlexibleContexts #-}    -- necessary for showFromF' example

 type family F    a
 type family FInv a

 -- This definition is accepted in 7.8 without anything extra, but requires
 -- AllowAmbiguousTypes in 7.10 (this, by itself, is not a problem):
 showFromF :: (Show a, FInv (F a) ~ a) => F a -> String
 showFromF fa = undefined

 -- Consider what happens when we attempt to call `showFromF` at some type
 b.
 -- In order to check that this is valid, we have to find an a such that
 --
 -- > b ~ F a /\ Show a /\ FInv (F a) ~ a
 --
 -- Introducing an intermeidate variable `x` for the result of `F a` gives
 us
 --
 -- > b ~ F a /\ Show a /\ FInv x ~ a /\ F a ~ x
 --
 -- Simplifying
 --
 -- > b ~ x /\ Show a /\ FInv x ~ a /\ F a ~ x
 --
 -- Set x := b
 --
 -- > Show a /\ FInv b ~ a /\ F a ~ b
 --
 -- Set a := FInv b
 --
 -- > Show (FInv b) /\ FInv b ~ FInv b /\ F (FInv b) ~ b
 --
 -- Simplifying
 --
 -- > Show (FInv b) /\ F (FInv b) ~ b
 --
 -- Indeed, we can give this definition in 7.8, but not in 7.10:
 showFromF' :: (Show (FInv b), F (FInv b) ~ b) => b -> String
 showFromF' = showFromF

 {-------------------------------------------------------------------------------
   In 7.10 the definition of showFromF' is not accepted, but it gets
 stranger.
   In 7.10 we cannot _call_ showFromF at all all, even at a concrete type.
 Below
   we try to call it at type b ~ Int. It would need to show
...
Show (FInv Int) /\ F (FInt Int) ~ Int
all of which should easily get resolved, but somehow don't.
 -------------------------------------------------------------------------------}

 type instance F    Int = Int
 type instance FInv Int = Int

 test :: String
 test = showFromF (0 :: Int)
 }}}

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10226
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler