[GHC] #15793: Type family doesn't reduce with visible kind application
#15793: Type family doesn't reduce with visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Keywords: | Operating System: Unknown/Multiple TypeApplications | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- If we un-comment `f2` {{{#!hs {-# Language RankNTypes #-} {-# Language TypeFamilies #-} {-# Language TypeApplications #-} {-# Language PolyKinds #-} import Data.Kind type family F1 (a :: Type) :: Type where F1 a = Maybe a f1 :: F1 a f1 = Nothing type family F2 :: forall (a :: Type). Type where F2 @a = Maybe a -- f2 :: F2 @a -- f2 = Nothing }}} this program fails with {{{ • Couldn't match kind ‘forall a1. *’ with ‘* -> *’ When matching types F2 :: forall a. * Maybe :: * -> * Expected type: F2 Actual type: Maybe a • In the expression: Nothing In an equation for ‘f2’: f2 = Nothing | 20 | f2 = Nothing | ^^^^^^^ Failed, no modules loaded. }}} It also succeeds replacing `Nothing` with `undefined` {{{#!hs f2 :: F2 @a f2 = undefined }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15793> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15793: Type family doesn't reduce with visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: invalid | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => closed * resolution: => invalid Comment: This is expected behavior. Your `F2` has an arity of 0 and so takes no argument, visible or otherwise. See related discussion in #11719. We don't yet have the syntax to declare a type family whose argument is both invisible and non-dependent. This would work fine internally, but there's just no way to say it. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15793#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15793: Type family doesn't reduce with visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: closed => new * resolution: invalid => Comment: But surely we should reject {{{ F2 @a = Maybe a }}} on the grounds that, well, `F2` has arity 0, so you can't supply an `@ty` arg on the left?
We don't yet have the syntax to declare a type family whose argument is both invisible and non-dependent.
Is another way to say this that the final argument of a type family must be `Required`; it cannot be `Specified`? What about `Inferred`? I think that is possible, isn't it? We should document this somehow in the user manual. Re-opening for these reasons. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15793#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15793: Type family doesn't reduce with visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #15740 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #15740 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15793#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15793: Type family doesn't reduce with visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #15740 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I think this is likely #15740, but you're right that I was too hasty in closing this. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15793#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15793: Type family doesn't reduce with visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.1 Resolution: fixed | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_compile/T15793 Blocked By: | Blocking: Related Tickets: #15740 | Differential Rev(s): Phab:D5229 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * testcase: => typecheck/should_compile/T15793 * status: new => closed * differential: => Phab:D5229 * resolution: => fixed * milestone: => 8.8.1 Comment: This was fixed in [https://gitlab.haskell.org/ghc/ghc/commit/17bd163566153babbf51adaff8397f948a... 17bd163566153babbf51adaff8397f948ae363ca]: {{{ Author: mynguyen <mnguyen1@brynmawr.edu> Date: Tue Dec 18 11:52:26 2018 -0500 Visible kind application Summary: This patch implements visible kind application (GHC Proposal 15/#12045), as well as #15360 and #15362. It also refactors unnamed wildcard handling, and requires that type equations in type families in Template Haskell be written with full type on lhs. PartialTypeSignatures are on and warnings are off automatically with visible kind application, just like in term-level. There are a few remaining issues with this patch, as documented in ticket #16082. Includes a submodule update for Haddock. Test Plan: Tests T12045a/b/c/TH1/TH2, T15362, T15592a Reviewers: simonpj, goldfire, bgamari, alanz, RyanGlScott, Iceland_jack Subscribers: ningning, Iceland_jack, RyanGlScott, int-index, rwbarton, mpickering, carter GHC Trac Issues: `#12045`, `#15362`, `#15592`, `#15788`, `#15793`, `#15795`, `#15797`, `#15799`, `#15801`, `#15807`, `#15816` Differential Revision: https://phabricator.haskell.org/D5229 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15793#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15793: Type family doesn't reduce with visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.1 Resolution: fixed | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_compile/T15793 Blocked By: | Blocking: Related Tickets: #15740 | Differential Rev(s): Phab:D5229 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Richard Eisenberg <rae@…>): In [changeset:"17bd163566153babbf51adaff8397f948ae363ca/ghc" 17bd1635/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="17bd163566153babbf51adaff8397f948ae363ca" Visible kind application Summary: This patch implements visible kind application (GHC Proposal 15/#12045), as well as #15360 and #15362. It also refactors unnamed wildcard handling, and requires that type equations in type families in Template Haskell be written with full type on lhs. PartialTypeSignatures are on and warnings are off automatically with visible kind application, just like in term-level. There are a few remaining issues with this patch, as documented in ticket #16082. Includes a submodule update for Haddock. Test Plan: Tests T12045a/b/c/TH1/TH2, T15362, T15592a Reviewers: simonpj, goldfire, bgamari, alanz, RyanGlScott, Iceland_jack Subscribers: ningning, Iceland_jack, RyanGlScott, int-index, rwbarton, mpickering, carter GHC Trac Issues: `#12045`, `#15362`, `#15592`, `#15788`, `#15793`, `#15795`, `#15797`, `#15799`, `#15801`, `#15807`, `#15816` Differential Revision: https://phabricator.haskell.org/D5229 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15793#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC