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 |
Edited by Icelandjack