[GHC] #11616: Kinds aren't instantiated

20 Feb 2016

      #11616: Kinds aren't instantiated
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:
               Type:  task           |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 {{{#!hs
 {-# LANGUAGE TypeInType, AllowAmbiugousTypes #-}

 class Whoami a where
   whoami :: String

 instance Whoami Int where
   whoami = "int"

 instance Whoami Bool where
   whoami = "[y/n]"

 instance Whoami Maybe where
   whoami = "call me maybe"
 }}}

 we can write

 {{{
...
...
...
whoami @Type @Int
 "int"
whoami @Type @Bool
 "[y/n]"
whoami @(Type -> Type) @Maybe
 "call me maybe"
 }}}
Attempting to specialise `whoami` to `Type` we can't simply write
 `whoamiType = whoami @Type` as one might expect. To start we define a
 synonym:

 {{{
 $ ghci -ignore-dot-ghci /tmp/t17q.hs
 GHCi, version 8.1.20160117: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling Main             ( /tmp/t17q.hs, interpreted )
 Ok, modules loaded: Main.
 *Main> whoami2 = whoami

 <interactive>:1:1: error:
     • Ambiguous type variable ‘a0’ arising from a use of ‘whoami’
       prevents the constraint ‘(Whoami a0)’ from being solved.
       Probable fix: use a type annotation to specify what ‘k0’, ‘a0’
 should be.
       These potential instances exist:
         three instance involving out-of-scope typess
         (use -fprint-potential-instances to see them all)
     • When instantiating ‘whoami2’, initially inferred to have
       this overly-general type:
         forall k (a :: k). Whoami a => String
       NB: This instantiation can be caused by the monomorphism
 restriction.
 }}}

 Using the “overly-general” inferred type `whoami :: forall k (a :: k).
 Whoami a => String` fails:

 {{{#!hs
 -- • Could not deduce (Whoami a0) arising from a use of ‘whoami’
 --   from the context: Whoami a
 --     bound by the type signature for:
 --                whoami2 :: Whoami a => String
 --      at /tmp/t17q.hs:20:1-44
 --   The type variable ‘a0’ is ambiguous
 --   These potential instances exist:
 --     three instance involving out-of-scope typess
 --     (use -fprint-potential-instances to see them all)
 -- • In the expression: whoami
 --   In an equation for ‘whoami2’: whoami2 = whoami

 whoami2 :: forall k (a :: k). Whoami a => String
 whoami2 = whoami
 }}}

 so we need `TypeApplications`:

 {{{#!hs
 whoami2 :: forall k (a :: k). Whoami a => String
 whoami2 = whoami @_ @a
 }}}

 and then we can write:

 {{{#!hs
 whoamiType :: forall (a :: Type). Whoami a => String
 whoamiType = whoami @_ @a
 }}}

 and we can write as intended:

 {{{
...
...
...
whoamiType @Int
 "int"
whoamiType @Bool
 "[y/n]"
 }}}
Is there a reason one cannot write:

 {{{#!hs
 whoami2 = whoami
 whoamiType = whoami @Type
 }}}

 ----

 As a side note, what is the difference between

 {{{#!hs
 -- >>> :set -fprintf-explicit-foralls
 -- >>> :kind Whoami1
 -- Whoami1 :: forall {k}. k -> Constraint
 -- >>> :kind Whoami2
 -- Whoami2 :: forall k.   k -> Constraint
 class Whoami1 a
 class Whoami2 (a :: k)
 }}}

 Is there a snippet of code that highlights differences

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