[GHC] #11616: Kinds aren't instantiated
GHC
ghc-devs at haskell.org
Sat Feb 20 21:30:51 UTC 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
More information about the ghc-tickets
mailing list