[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

#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
participants (1)
-
GHC