Opened 11 months ago

Closed 9 months ago

Last modified 8 months ago

#15793 closed bug (fixed)

Type family doesn't reduce with visible kind application

Reported by: Iceland_jack Owned by:
Priority: normal Milestone: 8.8.1
Component: Compiler Version: 8.6.1
Keywords: TypeApplications Cc: mnguyen
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:

Description

If we un-comment f2

{-# 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

f2 :: F2 @a
f2 = undefined

Change History (6)

comment:1 Changed 11 months ago by goldfire

Resolution: invalid
Status: newclosed

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.

comment:2 Changed 11 months ago by simonpj

Resolution: invalid
Status: closednew

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.

comment:3 Changed 11 months ago by RyanGlScott

comment:4 Changed 11 months ago by goldfire

I think this is likely #15740, but you're right that I was too hasty in closing this.

comment:5 Changed 9 months ago by RyanGlScott

Differential Rev(s): Phab:D5229
Milestone: 8.8.1
Resolution: fixed
Status: newclosed
Test Case: typecheck/should_compile/T15793

This was fixed in 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

comment:6 Changed 8 months ago by Richard Eisenberg <rae@…>

In 17bd1635/ghc:

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
Note: See TracTickets for help on using tickets.