Kinds aren't instantiated

{-# 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:

-- • 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:

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

and then we can write:

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:

whoami2 = whoami
whoamiType = whoami @Type

---

As a side note, what is the difference between

-- >>> :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

Trac metadata

Trac field	Value
Version	8.1
Type	Task
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture