[GHC] #14832: QuantifiedConstraints: Adding to the context causes failure

[GHC]

#14832: QuantifiedConstraints: Adding to the context causes failure
-------------------------------------+-------------------------------------
        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 Iceland_jack):

 Replying to [comment:12 simonpj]:
 > You want to write a ''term-level'' function that can be used a theorem
 in solving ''type-level'' constraints.

 That's right.

 Here are some thoughts I have on a
 [https://gist.github.com/ekmett/b26363fc0f38777a637d#file-categories-
 hs-L84 meatier example] I just ran into. Each category in `hask` has an
 associated constraint for objects (`Ob cat a`). If `a` is an object of
 `Dom f` and `f` is a functor then `f a` must be an object of `Cod f`

 {{{#!hs
 ob :: Functor f => Ob (Dom f) a :- Ob (Cod f) (f a)
 ob = Sub (source (fmap id))
 }}}

 Constructing this relies crucially on `fmap` and friends at the term
 level.

 The user has to pry `ob` open (at the right type) (here they just wanted
 to write `id = Nat id`)

 {{{#!hs
   id = Nat id1 where
     id1 :: forall f x. (Functor f, Ob (Dom f) x) => Cod f (f x) (f x)
     id1 = id \\ (ob :: Ob (Dom f) x :- Ob (Cod f) (f x))
 }}}

 It actually works today to add this implication to the superclass context
 of `Functor f` but GHC will not use it and refuses to take our (term-
 level) `ob` into account

 {{{#!hs
 type MapOb f = (forall x. Ob (Dom f) x => Ob (Cod f) (f x) :: Constraint)

 class (MapOb f, ..) => Functor f ..
 }}}

 I see several issues for what I just presented

 1. `Dom` / `Cod` are type families (#14860)
 2. We can't convert from `a :- b` to `Dict (a => b)` (#14822)
 3. Ignoring **1.** / **2.** for now, how can we even use `ob` to witness
 `MapOb f`?

 One idea is to allow pattern matching outside of `case` expressions or
 indeed outside any definition, so we could write

 {{{#!hs
 reifyC :: (a :- b) -> Dict (a => b)
 reifyC = error "let's assume this for a second"

 class MapOb f => Functor f where

   -- This brings `MapOb f' into scope for the whole instance
   Dict <- reifyC (ob @_ @_ @f)
 }}}

 Am I off base here?

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