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 |