[GHC] #14958: QuantifiedConstraints: Doesn't apply implication for existential?

GHC ghc-devs at haskell.org
Thu Mar 22 10:57:34 UTC 2018


#14958: QuantifiedConstraints: Doesn't apply implication for existential?
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.5
      Resolution:                    |             Keywords:
                                     |  QuantifiedConstraints, wipT2893
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 simonpj):

 This is to do with overlapping instances.  We have
 {{{
   Foo :: (forall x. ((forall y. cls y => Num y), cls x) => x) -> Foo
 }}}
 So from the expression `Foo 10` we have:
 Given:
 {{{
   Skolems: x
   Given:  d1: forall y. cls0 y => Num y
           d2: cls0 x

   Wanted: Num x
 }}}
 Here `cls0` is a unification variable; we don't yet know what it'll tur
 out to be, and indeed (given the type of `Foo`) it's ambiguous.

 When trying to solve `Num x` GHC doesn't want to use `d1`, because that
 make a commitment to solve its sub-goals.  If `cls0` turned out to be
 `Num`, an alternative would be to pick `d2`.  So it simply refrains from
 choosing.  (The error message doesn't make this clear, I know.)

 If you fix `cls0` all is well.  For example:
 {{{
 data Foo (cls :: * -> Constraint) where
   Foo :: forall cls.
            (forall x. ((forall y. cls y => Num y), cls x) => x)
            -> Foo cls

 a :: Foo Fractional
 a = Foo 10
 }}}

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


More information about the ghc-tickets mailing list