Question about TypeInType

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

Question about TypeInType

Iavor Diatchki
Hello,

I was experimenting with TypeInType and run into a problem, that can be reduced to the following example.  Does anyone have any insight on what causes the error, in particular why is `IxKind` not being reduced?

-Iavor


{-# Language TypeInType, TypeFamilies #-}

module Help where

import Data.Kind

type family IxKind (m :: Type) :: Type
type family Value (m :: Type) :: IxKind m -> Type

data T (k :: Type) (f :: k -> Type)

type instance IxKind (T k f) = k
type instance Value (T k f) = f

{-
[1 of 1] Compiling Help             ( Desktop/Help.hs, interpreted )
Desktop/Help.hs:13:31: error:
    • Expected kind ‘IxKind (T k f) -> *’, but ‘f’ has kind ‘k -> *’
    • In the type ‘f’
      In the type instance declaration for ‘Value’
   |
13 | type instance Value (T k f) = f
   |                               ^
Failed, no modules loaded.
-}

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Question about TypeInType

Richard Eisenberg-4
I think this is #12088. The problem is that open type family instances aren't used in kind checking in the same region of a module. The workaround is to put a top-level Template Haskell splice

> $(return [])

between the two type instances. This is far from optimal, but fixing it is a Major Project. See https://ghc.haskell.org/trac/ghc/ticket/12088#comment:15

Richard

On Apr 12, 2018, at 7:47 PM, Iavor Diatchki <[hidden email]> wrote:

Hello,

I was experimenting with TypeInType and run into a problem, that can be reduced to the following example.  Does anyone have any insight on what causes the error, in particular why is `IxKind` not being reduced?

-Iavor


{-# Language TypeInType, TypeFamilies #-}

module Help where

import Data.Kind

type family IxKind (m :: Type) :: Type
type family Value (m :: Type) :: IxKind m -> Type

data T (k :: Type) (f :: k -> Type)

type instance IxKind (T k f) = k
type instance Value (T k f) = f

{-
[1 of 1] Compiling Help             ( Desktop/Help.hs, interpreted )
Desktop/Help.hs:13:31: error:
    • Expected kind ‘IxKind (T k f) -> *’, but ‘f’ has kind ‘k -> *’
    • In the type ‘f’
      In the type instance declaration for ‘Value’
   |
13 | type instance Value (T k f) = f
   |                               ^
Failed, no modules loaded.
-}
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

RE: Question about TypeInType

GHC - devs mailing list

if it is, please can someone add a new regression example to #12088.  You can never have too many.

 

Thanks

 

Simon

 

From: ghc-devs <[hidden email]> On Behalf Of Richard Eisenberg
Sent: 13 April 2018 02:39
To: Iavor Diatchki <[hidden email]>
Cc: [hidden email]
Subject: Re: Question about TypeInType

 

I think this is #12088. The problem is that open type family instances aren't used in kind checking in the same region of a module. The workaround is to put a top-level Template Haskell splice

 

> $(return [])

 

between the two type instances. This is far from optimal, but fixing it is a Major Project. See https://ghc.haskell.org/trac/ghc/ticket/12088#comment:15

 

Richard



On Apr 12, 2018, at 7:47 PM, Iavor Diatchki <[hidden email]> wrote:

 

Hello,

 

I was experimenting with TypeInType and run into a problem, that can be reduced to the following example.  Does anyone have any insight on what causes the error, in particular why is `IxKind` not being reduced?

 

-Iavor

 

 

{-# Language TypeInType, TypeFamilies #-}

 

module Help where

 

import Data.Kind

 

type family IxKind (m :: Type) :: Type

type family Value (m :: Type) :: IxKind m -> Type

 

data T (k :: Type) (f :: k -> Type)

 

type instance IxKind (T k f) = k

type instance Value (T k f) = f

 

{-

[1 of 1] Compiling Help             ( Desktop/Help.hs, interpreted )

Desktop/Help.hs:13:31: error:

    • Expected kind ‘IxKind (T k f) -> *’, but ‘f’ has kind ‘k -> *’

    • In the type ‘f’

      In the type instance declaration for ‘Value’

   |

13 | type instance Value (T k f) = f

   |                               ^

Failed, no modules loaded.

-}

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

 


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Question about TypeInType

Richard Eisenberg-4
Done.

On Apr 16, 2018, at 11:08 AM, Simon Peyton Jones <[hidden email]> wrote:

if it is, please can someone add a new regression example to #12088.  You can never have too many.
 
Thanks
 
Simon
 
From: ghc-devs <[hidden email]> On Behalf Of Richard Eisenberg
Sent: 13 April 2018 02:39
To: Iavor Diatchki <[hidden email]>
Cc: [hidden email]
Subject: Re: Question about TypeInType
 
I think this is #12088. The problem is that open type family instances aren't used in kind checking in the same region of a module. The workaround is to put a top-level Template Haskell splice
 
> $(return [])
 
between the two type instances. This is far from optimal, but fixing it is a Major Project. See https://ghc.haskell.org/trac/ghc/ticket/12088#comment:15
 
Richard


On Apr 12, 2018, at 7:47 PM, Iavor Diatchki <[hidden email]> wrote:
 
Hello,
 
I was experimenting with TypeInType and run into a problem, that can be reduced to the following example.  Does anyone have any insight on what causes the error, in particular why is `IxKind` not being reduced?
 
-Iavor
 
 
{-# Language TypeInType, TypeFamilies #-}
 
module Help where
 
import Data.Kind
 
type family IxKind (m :: Type) :: Type
type family Value (m :: Type) :: IxKind m -> Type
 
data T (k :: Type) (f :: k -> Type)
 
type instance IxKind (T k f) = k
type instance Value (T k f) = f
 
{-
[1 of 1] Compiling Help             ( Desktop/Help.hs, interpreted )
Desktop/Help.hs:13:31: error:
    • Expected kind ‘IxKind (T k f) -> *’, but ‘f’ has kind ‘k -> *’
    • In the type ‘f’
      In the type instance declaration for ‘Value’
   |
13 | type instance Value (T k f) = f
   |                               ^
Failed, no modules loaded.
-}
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs