
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. -}

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 https://ghc.haskell.org/trac/ghc/ticket/12088#comment:15 Richard
On Apr 12, 2018, at 7:47 PM, Iavor Diatchki
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 ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

if it is, please can someone add a new regression example to #12088. You can never have too many.
Thanks
Simon
From: ghc-devs
$(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

Done.
On Apr 16, 2018, at 11:08 AM, Simon Peyton Jones
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
On Behalf Of Richard Eisenberg Sent: 13 April 2018 02:39 To: Iavor Diatchki Cc: ghc-devs@haskell.org 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 https://ghc.haskell.org/trac/ghc/ticket/12088#comment:15
Richard
On Apr 12, 2018, at 7:47 PM, Iavor Diatchki
mailto:iavor.diatchki@gmail.com> 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 ghc-devs@haskell.org mailto:ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
participants (3)
-
Iavor Diatchki
-
Richard Eisenberg
-
Simon Peyton Jones