[GHC] #16116: Explicit foralls in associated type family equations are oblivious to class-bound variables

[GHC]

#16116: Explicit foralls in associated type family equations are oblivious to
class-bound variables
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.7
      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:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 That example is rejected with a `Not in scope: type variable ‘b’` error,
 before and after the patch, since `b` is simply not bound anywhere.

 A more interesting example is the one from `T5515`:

 {{{#!hs
 instance ctx a => Bome ctx where
   type BArg ctx = a
 }}}

 This time, `a` technically //is// in scope over the type family equation.
 However, it's not bound on the LHS of the equation, so it's rejected.
 After this patch, the new error message becomes:

 {{{#!diff
 diff -uw "indexed-types/should_fail/T5515.run/T5515.stderr.normalised"
 "indexed-types/should_fail/T5515.run/T5515.comp.stderr.normalised"
 --- indexed-types/should_fail/T5515.run/T5515.stderr.normalised 2019-01-09
 11:08:03.005471816 -0500
 +++ indexed-types/should_fail/T5515.run/T5515.comp.stderr.normalised
 2019-01-09 11:08:03.005471816 -0500
 @@ -1,8 +1,24 @@

 -T5515.hs:9:3:
 -    The RHS of an associated type declaration mentions out-of-scope
 variable ‘a’
 -      All such variables must be bound on the LHS
 +T5515.hs:6:16:
 +     Expecting one more argument to ‘ctx’
 +      Expected a type, but ‘ctx’ has kind ‘* -> Constraint’
 +     In the first argument of ‘Arg’, namely ‘ctx’
 +      In the first argument of ‘ctx’, namely ‘(Arg ctx)’
 +      In the class declaration for ‘Bome’

 -T5515.hs:15:3:
 -    The RHS of an associated type declaration mentions out-of-scope
 variable ‘a’
 -      All such variables must be bound on the LHS
 +T5515.hs:14:1:
 +     Type variable ‘a’ is mentioned in the RHS,
 +        but not bound on the LHS of the family instance
 +     In the type instance declaration for ‘Arg’
 +      In the instance declaration for ‘Some f’
 +
 +T5515.hs:14:10:
 +     Could not deduce (C f a0)
 +      from the context: C f a
 +        bound by an instance declaration:
 +                   forall f a. C f a => Some f
 +        at T5515.hs:14:10-24
 +      The type variable ‘a0’ is ambiguous
 +     In the ambiguity check for an instance declaration
 +      To defer the ambiguity check to use sites, enable
 AllowAmbiguousTypes
 +      In the instance declaration for ‘Some f’
 }}}

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