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,252
    • Issues 5,252
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 576
    • Merge requests 576
  • 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
  • #12905
Closed
Open
Issue created Nov 30, 2016 by Ben Gamari@bgamari🐢Maintainer

Core lint failure with pattern synonym and levity polymorphism

Yet another program from the type-indexed Typeable effort which breaks GHC (master branch as of 3bd1dd4d) with a core lint error,

{-# LANGUAGE GADTs, TypeOperators, PatternSynonyms, TypeInType, PolyKinds, RankNTypes #-}
module T where

import GHC.Exts
import Data.Kind
import Data.Type.Equality

data TypeRep (a :: k) where
    TrTyCon :: TypeRep (a :: k)
    TrApp   :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
               TypeRep (a :: k1 -> k2)
            -> TypeRep (b :: k1)
            -> TypeRep (a b)
    TrFun   :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (a :: TYPE r1) (b :: TYPE r2).
               TypeRep a
            -> TypeRep b
            -> TypeRep (a -> b)

pattern TRFun :: forall k (fun :: k). ()
              => forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (arg :: TYPE r1) (res :: TYPE r2). (k ~ Type, fun ~~ (arg -> res))
              => TypeRep arg
              -> TypeRep res
              -> TypeRep fun
pattern TRFun arg res <- TrFun arg res
  where TRFun arg res = TrFun arg res

This program produces many core lint errors, although all of them fall into only a few classes. Here's one,

*** Core Lint errors : in result of Desugar (before optimization) ***
<no location info>: warning:
    In the coercion ‘Sym (Sym cobox_a3fT |> Sym cobox_a3fU)’
    Kind application error in
      type ‘((->) |> <*>_N ->_N <*>_N ->_N Sym cobox) a’
      Function kind = * -> * -> k
      Arg kinds = [(a, TYPE r1)]
<no location info>: warning:
    [RHS of $d~~_a3fO :: (fun :: k) ~~ ((a -> b) :: *)]
    Kind application error in
      coercion ‘Sym
                  (Sym
                     (<(->)>_N |> ((<*>_N -> <*>_N -> Sym cobox_a3fU)
                                   ; Sym (<*>_N -> <*>_N -> Sym cobox_a3fH))) |> (<*>_N
                                                                                  -> <*>_N
                                                                                  -> Sym
                                                                                       cobox_a3fU)) <a>_N’
      Function kind = * -> * -> *
      Arg kinds = [(a, TYPE r1)]

This may be yet another case of the kind of (->) being too restrictive (#11714 (closed)) since a -> b appears to be lifted to the coercion TyConAppCo role (->) [a, b].

Edited Mar 10, 2019 by Ben Gamari
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking