Opened 6 weeks ago

Last modified 5 weeks ago

#14556 new bug

Core Lint error: Ill-kinded result in coercion

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.3
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #14554 Differential Rev(s):
Wiki Page:

Description

{-# Language UndecidableInstances, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #-}

import Data.Kind
import Data.Proxy

data Fn a b where
  IdSym :: Fn Type Type

type family
  (@@) (f::Fn k k') (a::k)::k' where
  IdSym @@ a = a

data KIND = X | FNARR KIND KIND

data TY :: KIND -> Type where
  ID    :: TY (FNARR X X)
  FNAPP :: TY (FNARR k k') -> TY k -> TY k'

data TyRep (kind::KIND) :: TY kind -> Type where
  TID    :: TyRep (FNARR X X)  ID
  TFnApp :: TyRep (FNARR k k') f
         -> TyRep k            a
         -> TyRep k'           (FNAPP f a)

type family
  IK (kind::KIND) :: Type where
  IK X            = Type
  IK (FNARR k k') = Fn (IK k) (IK k')

type family
  IT (ty::TY kind) :: IK kind where
  IT ID          = IdSym
  IT (FNAPP f x) = IT f @@ IT x

zero :: TyRep X a -> IT a
zero = undefined 

which gives Core lint error when run with ghci -ignore-dot-ghci -dcore-lint (8.3.20171122) attached.

It compiles fine with

zero :: TyRep X a -> IT a
zero = zero

but fails with zero = let x = x in x. See #14554.

Attachments (1)

bug.log (8.2 KB) - added by Iceland_jack 6 weeks ago.

Download all attachments as: .zip

Change History (2)

Changed 6 weeks ago by Iceland_jack

Attachment: bug.log added

comment:1 Changed 5 weeks ago by simonpj

I think this is another example of the bugs surrounding "flattened types have flattened kinds". What is happening is this. In the RHS of zero we get a constraint

    [W} (alpha :: TYPE r)  ~  TyRep X a -> (IT a |> ax_IK)
where
    ax_IK :: IK X ~ Type   -- Just an axiom for IK

which should strainghtforwardly unify. But before we do that we flatten (IT a |> ax_IK), but alas we get just

     (fuv :: IK X)
where
     fuv = IT a     -- CFunEqCan

The cast has disappeared. This happens in TcFlatten:

flatten_one (CastTy ty g)

I'm pretty sure it's just another manifestation of our existing set of bugs around flattening (Trac #12919). Richard has a mostly-finished patch that cures this --- it'd be great to get it finished!

Note: See TracTickets for help on using tickets.