Kind signature not accepted (singletons)
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.
Trac metadata
Trac field | Value |
---|---|
Version | 8.2.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |