Opened 5 weeks ago

Closed 5 weeks ago

Last modified 5 weeks ago

#14139 closed bug (duplicate)

Kind signature not accepted (singletons)

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

Description

I don't understand the rules for kind signatures / CUSKs but this works

import Data.Singletons.Prelude

data Some (f :: u ~> v) where
  Some :: Sing (x :: u) -> f @@ x -> Some f

but this doesn't?

import Data.Kind
import Data.Singletons.Prelude

data Some :: (u ~> v) -> Type where
  Some :: Sing (x :: u) -> f @@ x -> Some f

--        • Expected kind ‘u ~> v’, but ‘f’ has kind ‘u ~> *’
--        • In the first argument of ‘Some’, namely ‘f’
--          In the type ‘Some f’
--          In the definition of data constructor ‘Some’
--      |
--    5 |   Some :: Sing (x :: u) -> f @@ x -> Some f
--      |                                           ^
--    Failed, modules loaded: none.

I have to quantify over them for it to work forall u v. (u ~> v) -> Type, if this is expected I feel like the error message ought to be improved.

Change History (4)

comment:1 Changed 5 weeks ago by Iceland_jack

Keywords: TypeInType added
Summary: Kind signatureKind signature not accepted (singletons)

comment:2 Changed 5 weeks ago by RyanGlScott

Resolution: duplicate
Status: newclosed

Yep, this is a CUSK issue. Here is the relevant section of the users' guide:

-  For a datatype with a top-level ``::`` when :ghc-flag:`-XTypeInType`
   is in effect: all kind variables introduced after the ``::`` must
   be explicitly quantified. ::

     -- -XTypeInType is on
     data T1 :: k -> *            -- No CUSK: `k` is not explicitly quantified
     data T2 :: forall k. k -> *  -- CUSK: `k` is bound explicitly
     data T3 :: forall (k :: *). k -> *   -- still a CUSK

   Note that the first example would indeed have a CUSK without
   :ghc-flag:`-XTypeInType`.

In your example, v is not explicitly quantified in the kind signature of Some, which explains why its kind defaults to * (and results in the error message you see).

Since this asks to improve the error message to warn about CUSK behavior, I'll close this as a duplicate of #13365, which seeks the same goal.

comment:3 Changed 5 weeks ago by RyanGlScott

Keywords: CUSKs added

comment:4 Changed 5 weeks ago by Iceland_jack

Thanks!!

Note: See TracTickets for help on using tickets.