Re: [GHC] #11948: GHC forgets constraints

17 Apr 2016


      #11948: GHC forgets constraints
-------------------------------------+-------------------------------------
        Reporter:  crockeea          |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.0.2
       Component:  Compiler          |              Version:  7.10.3
      Resolution:                    |             Keywords:
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:                    |
-------------------------------------+-------------------------------------
Changes (by bgamari):

 * milestone:   => 8.0.2


@@ -24,1 +24,1 @@
- Main.hs:
+ **Main.hs:**
@@ -26,1 +26,1 @@
- {{{
+ {{{#!hs
@@ -28,0 +28,2 @@
+
+ module Main where
@@ -39,1 +41,1 @@
- Bar.hs
+ **Bar.hs**
@@ -41,1 +43,1 @@
- {{{
+ {{{#!hs

New description:

 Possibly related: #10338

 The following program should compile, but fails with the error:

 {{{
 Could not deduce (Bar (F zq) zq) arising from a use of ‘bar’
     from the context (Bar (Foo (F zq)) (Foo zq))
       bound by the type signature for
                  bug :: Bar (Foo (F zq)) (Foo zq) => Foo (F zq) -> Foo zq
 }}}

 This is definitely incorrect: I am providing a `Bar` constraint in the
 context of `bug`, but GHC is asking for constraints so that it can resolve
 to the instance declared in Bar.hs.

 A few workarounds I've found so far, which may or may not help find the
 bug:
 1. Adding `-XTypeFamilies` to Main.hs makes the program compile.
 2. ''Removing'' the type signature from `x` in `bug` makes the program
 compile.
 3. Defining `bug` without a `let` as `bug sk = bar sk :: Foo zq` or `bug
 sk = bar sk` makes the program compile.

 **Main.hs:**

 {{{#!hs
 {-# LANGUAGE FlexibleContexts, ScopedTypeVariables #-}

 module Main where

 import Bar

 bug :: forall zq .
   (Bar (Foo (F zq)) (Foo zq))
   => Foo (F zq) -> Foo zq
 bug sk =
   let x = bar sk :: Foo zq
   in x
 }}}

 **Bar.hs**

 {{{#!hs
 {-# LANGUAGE MultiParamTypeClasses, TypeFamilies #-}

 module Bar where

 type family F b

 newtype Foo r = Foo r

 type instance F (Foo r) = Foo (F r)

 class Bar a b where
   bar :: a -> b

 instance (Bar a b) => Bar (Foo a) (Foo b)
 }}}

--

Comment:

 This is reproducible with 8.0.1-rc3.

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

    