Re: [GHC] #12025: Order of constraints forced (in pattern synonyms, type classes in comments)

9 May 2016

      #12025: Order of constraints forced (in pattern synonyms, type classes in comments)
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.1
  checker)                           |             Keywords:
      Resolution:                    |  TypeApplications PatternSynonyms
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  11513, 10928      |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Iceland_jack):

 8.1.20160503

 {{{
 ghci> class P (p :: Type -> Type) where pee :: p a -> Int

 ghci> :set -fprint-explicit-foralls
 ghci> :t pee
 pee :: forall {a} {p :: Type -> Type}. P p => p a -> Int
 }}}

 `a` appears before `p`, but does not apply in that order? This is
 surprising behaviour to me:

 {{{
 ghci> instance P Maybe where pee = length

 ghci> :t pee @Maybe
 pee @Maybe :: forall {a}. Maybe a -> Int
 ghci> :t pee @Maybe @()
 pee @Maybe @() :: Maybe () -> Int
 }}}

 ----

 Replying to [comment:4 goldfire]:
...
As for classes, I'm not as bothered. The workaround is straightforward.
I wonder if you could just mention the variable before the instance but
 that is disallowed in `class` declarations. Something silly `class a ~ a
 => P p where pee :: p a -> Int`.

 By accident I saw the ticket #6081 which quantifies in the instance
 signature:

 {{{#!hs
 instance forall (a :: k). KindClass (KP :: KProxy [k])
 }}}

 I had no idea this was allowed, it seems to only refer to variables in the
 instance head, when I try to use it:

 {{{#!hs
 -- error:
 --   • Couldn't match type ‘a1’ with ‘a’
 instance forall a. P Maybe where
   pee :: Maybe a -> Int
   pee = length
 }}}

 Currently disallowed in class declarations, but what if

 {{{#!hs
 class forall a. P (p :: Type -> Type) where
   pee :: p a -> Int
 }}}

 meant that `a` appears before `p` in methods? The downside is that this
 would apply to every method across the board leaving no way to write
 siblings with a different order

 {{{#!hs
 class Q q where
   cue_1 :: q a -> Int
   cue_2 :: q a -> Int

 -- cue_1 :: forall q a. Q q => q a -> Int
 -- cue_1 :: forall a q. Q q => q a -> Int
 }}}

 This may just be inherent in the way type classes are structured, reminds
 me of Idris' [http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html
 #using-notation ‘using’ notation]. In broken Idris:

 {{{#!hs
 using (q:Type -> Type)
   using (a:Type)
     cue_1 : q a -> Int
     cue_2 : q a -> Int

 using (a:Type)
   using (q:Type -> Type)
     cue_1 : q a -> Int
     cue_2 : q a -> Int
 }}}

 It isn't a show-stopper for type classes as Richard says, just nice to
 have. I hadn't even thought of record selectors.

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