[GHC] #9725: Constraint deduction failure

[GHC]

#9725: Constraint deduction failure
-------------------------------------+-------------------------------------
       Reporter:  heisenbug          |                   Owner:
           Type:  bug                |                  Status:  new
       Priority:  normal             |               Milestone:
      Component:  Compiler (Type     |                 Version:  7.8.3
  checker)                           |        Operating System:
       Keywords:                     |  Unknown/Multiple
   Architecture:  Unknown/Multiple   |         Type of failure:  GHC
     Difficulty:  Unknown            |  rejects valid program
     Blocked By:                     |               Test Case:
Related Tickets:                     |                Blocking:
                                     |  Differential Revisions:
-------------------------------------+-------------------------------------
 I get a strange error message like this

 {{{
 [1 of 1] Compiling Main             ( 08-10.hs, interpreted )

 08-10.hs:254:33:
     Could not deduce (KnownLoc (ent par1 a))
       arising from a use of ‘Hidden'’
     from the context (List ConfFamily ts)
       bound by the type signature for
                  locAware :: List ConfFamily ts =>
                              (forall (i :: k).
                               KnownLoc (ent par i) =>
                               ConfFamily (Facility (ent par i)) ts)
                              -> Con ConfFamily (On ent par)
       at 08-10.hs:251:13-160
     or from (ent par a ~ 'Monitor par1 mp, KnownLoc ('Monitor par1 mp))
       bound by a pattern with constructor
                  MonitorF :: forall (par :: Entity) (mp :: MonitorPoint).
                              KnownLoc ('Monitor par mp) =>
                              String -> String -> Observer -> Bool ->
 Facility ('Monitor par mp),
                in an equation for ‘h’
       at 08-10.hs:254:19-28
     In the expression: Hidden' (d f)
     In an equation for ‘h’: h (Hide f@(MonitorF {})) = Hidden' (d f)
     In an equation for ‘locAware’:
         locAware descr
           = Abstr h
           where
               h :: (ent `On` par) -> ConfFamily (ent `On` par) ts
               h (Hide f@(MonitorF {})) = Hidden' (d f)
               d ::
                 KnownLoc (ent par i) =>
                 Facility (ent par i) -> ConfFamily (Facility (ent par i))
 ts
               d _ = descr
 Failed, modules loaded: none.
 }}}

 I have many language extensions active, such as, `DataKinds`,
 `ScopedTypeVariables`, etc.

 If somebody says this indeed looks like a bug, then I'll try to post a
 minimal reproduction case.

 ** My reasoning goes like this **

 Here are the relevant facts that GHC figured out from a GADT pattern
 match:
 `(ent par a ~ 'Monitor par1 mp, KnownLoc ('Monitor par1 mp))`

 From this I discover these equalities:
 {{{
 ent === 'Monitor    (*)
 par === par1        (**)
 a === mp            (***)
 }}}
 Substituring `(*)`^-1^ and `(***)`^-1^ into the given `KnownLoc ('Monitor
 par1 mp)` results in the desired `KnownLoc (ent par1 a)`

 Looks like a bug, right?

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