Opened 2 years ago

Closed 2 years ago

Last modified 7 months ago

#9357 closed bug (fixed)

Kind-polymorphic type family accepts unlifted type arguments

Reported by: kosmikus Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.8.2
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC accepts invalid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

The following code is accepted by ghc-7.8.2 and ghc-7.6.3:

{-# LANGUAGE TypeFamilies, MagicHash, PolyKinds #-}

import GHC.Exts

type family F (a :: k) :: *
type instance F Int# = ()

In nearly all other places, it seems that unlifted types are explicitly forbidden. I'm also not allowed to actually apply F to Int# after defining the type family like this. So I think the compiler should probably reject the type instance.

(BTW, is it actually clear that using # as an argument kind to a type family or as an index kind for a GADT is in any way harmful?)

Change History (4)

comment:1 Changed 2 years ago by Simon Peyton Jones <simonpj@…>

In a997f2df785448648e7137a88d6b38eeb2643aa1/ghc:

Check for boxed tau types in the LHS of type family instances

Fixes Trac #9357

comment:2 Changed 2 years ago by simonpj

Good point. It's not impossible that we could accept unboxed arguments to type families, but unbozed results would definitely be problematic: how many bits does it take to represent (F Int)? Is is held in an integer register or a floating point register.

For now I've just made it so that we require a boxed monotype as both argument and result.

Simon

comment:3 Changed 2 years ago by simonpj

  • Resolution set to fixed
  • Status changed from new to closed

comment:4 Changed 7 months ago by bgamari

If Phab:D1807 is merged then this limitation will once again be lifted allowing,

{-# LANGUAGE PolyKinds, TypeFamilies, MagicHash, DataKinds, TypeInType #-}

import GHC.Exts
import GHC.Types

type family Boxed (a :: k) :: *
type instance Boxed Char# = Char
type instance Boxed Char  = Char

class BoxIt (a :: TYPE lev) where
    boxed :: a -> Boxed a

instance BoxIt Char# where boxed x = C# x
instance BoxIt Char  where boxed = id

main :: IO ()
main = do
    print $ boxed 'c'#
    print $ boxed 'c'

Last edited 7 months ago by bgamari (previous) (diff)
Note: See TracTickets for help on using tickets.