Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 5,243
    • Issues 5,243
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 569
    • Merge requests 569
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell CompilerGlasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #12102
Closed
Open
Issue created May 22, 2016 by Icelandjack@IcelandjackReporter

“Constraints in kinds” illegal family application in instance (+ documentation issues?)

GHC 8.0.0.20160511. Example from the user guide: Constraints in kinds

type family IsTypeLit a where
  IsTypeLit Nat    = 'True
  IsTypeLit Symbol = 'True
  IsTypeLit a      = 'False

data T :: forall a. (IsTypeLit a ~ 'True) => a -> * where
  MkNat    :: T 42
  MkSymbol :: T "Don't panic!"

Deriving a standalone Show instance *without* the constraint (IsTypeLit a ~ 'True) => works fine

deriving instance Show (T a)

but I couldn't define a Show instance given the constraints:

-- • Couldn't match expected kind ‘'True’
--               with actual kind ‘IsTypeLit a0’
--   The type variable ‘a0’ is ambiguous
-- • In the first argument of ‘Show’, namely ‘T a’
--   In the stand-alone deriving instance for ‘Show (T a)’
deriving instance Show (T a)

let's add constraints

-- • Couldn't match expected kind ‘'True’
--               with actual kind ‘IsTypeLit lit’
-- • In the first argument of ‘Show’, namely ‘T (a :: lit)’
--   In the instance declaration for ‘Show (T (a :: lit))’
instance IsTypeLit lit ~ 'True => Show (T (a :: lit)) where

let's derive for a single literal

-- • Illegal type synonym family application in instance:
--     T Nat
--       ('Data.Type.Equality.C:~
--          Bool
--          (IsTypeLit Nat)
--          'True
--          ('GHC.Types.Eq# Bool Bool (IsTypeLit Nat) 'True <>))
--       42
-- • In the stand-alone deriving instance for ‘Show (T (42 :: Nat))’
deriving instance Show (T (42 :: Nat))

same happens with

instance Show (T 42) where

The documentation

Note that explicitly quantifying with forall a is not necessary here.

seems to be wrong since removing it results in

tVDv.hs:10:17-18: error: …
    • Expected kind ‘a’, but ‘42’ has kind ‘Nat’
    • In the first argument of ‘T’, namely ‘42’
      In the type ‘T 42’
      In the definition of data constructor ‘MkNat’
Compilation failed.
Edited Mar 10, 2019 by Icelandjack
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking