Opened 19 months ago

Closed 5 months ago

#11616 closed task (fixed)

Kinds aren't instantiated

Reported by: Iceland_jack Owned by:
Priority: normal Milestone: 8.2.1
Component: Compiler Version: 8.1
Keywords: TypeApplications Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D3531
Wiki Page:

Description

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

Change History (8)

comment:1 Changed 19 months ago by goldfire

This is almost correct behavior. The only incorrect part of this is that visible type application is available on the kind argument to whoami even though the kind variable was not written in the declaration of Whomami. You hint at this weirdness at the end of your post, where the braces mean that a variable is not available for visible type application (because GHC inferred its presence and ordering). This is a known bug that I intend to fix.

But everything else is OK. The problem is that visible type application should work on only type variables that are written by the user. (I have clarified this in unpushed edits to the manual.) When you say whoami2 = whoami, you're not giving a type signature to whoami2, and therefore usages of whoami2 cannot use visible type application. This design decision was made to help keep usage of visible type application retain the same meaning as GHC's inference algorithm evolves. Without visible type application, whoami2's type is indeed ambiguous and problematic.

The problem is the same with whoamiType. And indeed, if you give a type signature, all is OK:

whoamiType :: forall a. Whoami (a :: Type) => String
whoamiType = whoami @_ @a

I'm keeping this bug open to track the fix for the first issue, and as an interesting test case.

comment:2 Changed 19 months ago by simonpj

Keywords: TypeApplications added

comment:3 Changed 5 months ago by RyanGlScott

Is this bug still present? I just tried defining this:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeInType #-}
module T11616 where

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"

whoisint :: String
whoisint = whoami @Int

And compiling it works without a hitch on GHC 8.0.1, 8.0.2, 8.2.1, and HEAD. So I suspect that the invisible kind variable is no longer available for type application, which is the behavior you desire, right goldfire?

comment:4 Changed 5 months ago by goldfire

Agreed with the analysis in comment:3 -- this seems fixed. Is there a regression test somewhere before we close the ticket?

comment:5 Changed 5 months ago by RyanGlScott

Differential Rev(s): Phab:D3531
Status: newpatch

I couldn't find a test which adequately tested all of the features that this program uses, so I added one of my own in Phab:D3531.

comment:6 Changed 5 months ago by Ben Gamari <ben@…>

In 03ca391f/ghc:

Add regression test for #11616

The code in #11616 has been working for a while (ever since 8.0.1),
so let's add a regression test for it to put the nail in the coffin.

Test Plan: make test TEST=T11616

Reviewers: austin, bgamari

Reviewed By: bgamari

Subscribers: rwbarton, thomie

GHC Trac Issues: #11616

Differential Revision: https://phabricator.haskell.org/D3531

comment:7 Changed 5 months ago by bgamari

Milestone: 8.2.1
Status: patchmerge

comment:8 Changed 5 months ago by bgamari

Resolution: fixed
Status: mergeclosed
Note: See TracTickets for help on using tickets.