Opened 2 years ago

Closed 2 years ago

#6036 closed bug (fixed)

Kind generalization fails in data family instance GADT

Reported by: goldfire Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.5
Keywords: Cc: pho@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Difficulty: Unknown
Test Case: polykinds/T6036 Blocked By:
Blocking: Related Tickets:

Description

The following code fails to compile:

{-# LANGUAGE DataKinds, TypeFamilies, PolyKinds, GADTs #-}

data family Sing (a :: k)

data instance Sing (a :: Maybe k) where
  SNothing :: Sing 'Nothing
  SJust :: Sing b -> Sing ('Just b)

The error is

    Data constructor `SNothing' returns type `Sing
                                                (Maybe k0) ('Nothing k0)'
      instead of an instance of its parent type `Sing (Maybe k) a'
    In the definition of data constructor `SNothing'
    In the data instance declaration for `Sing'

It seems that the k kind parameter is not being allowed to generalize over other kind parameters. The following (seemingly equivalent) formulation compiles:

{-# LANGUAGE ..., ExistentialQuantification #-}

data instance Sing (a :: Maybe k) =
    a ~ 'Nothing => SNothing
  | forall b. a ~ 'Just b => SJust (Sing b)

This was tested on 7.5.20120420.

Change History (4)

comment:1 Changed 2 years ago by goldfire

The following code is another demonstration of (I believe) the same underlying problem:

{-# LANGUAGE DataKinds, TypeFamilies, PolyKinds, GADTs, ExistentialQuantification #-}

data Nat = Zero | Succ Nat

data family Sing (a :: k)

data instance Sing (a :: Nat) where
  SZero :: Sing Zero
  SSucc :: Sing n -> Sing (Succ n)

data instance Sing (a :: Maybe k) =
    a ~ 'Nothing => SNothing
  | forall b. a ~ 'Just b => SJust (Sing b)

term = SJust SZero

The last line fails with the following:

    Couldn't match kind `k' against `Nat'
    Kind incompatibility when matching types:
      b0 :: k
      'Zero :: Nat
    In the first argument of `SJust', namely `SZero'
    In the expression: SJust SZero

comment:2 Changed 2 years ago by PHO

  • Cc pho@… added

comment:3 Changed 2 years ago by simonpj@…

commit 2316a90da6e78349874a181baa762ef60c80333e

Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Wed Apr 25 12:56:44 2012 +0100

    More fixes to kind polymorphism, fixes Trac #6035, #6036
    
    * Significant refactoring in tcFamPats and tcConDecl
    
    * It seems that we have to allow KindVars (not just
      TcKindVars during kind unification.  See
      Note [Unifying kind variables] in TcUnify.
    
    * Be consistent about zonkQuantifiedTyVars
    
    * Split the TcType->TcType zonker (in TcMType)
       from the TcType->Type   zonker (in TcHsSyn)
      The clever parameterisation was doing my head in,
      and it's only a small function
    
    * Remove some dead code (tcTyVarBndrsGen)

 compiler/ghci/RtClosureInspect.hs   |    4 +-
 compiler/typecheck/FamInst.lhs      |   11 ++--
 compiler/typecheck/TcHsSyn.lhs      |   90 ++++++++++++++++-----------
 compiler/typecheck/TcHsType.lhs     |   65 ++++++++-----------
 compiler/typecheck/TcMType.lhs      |   79 ++++++++---------------
 compiler/typecheck/TcTyClsDecls.lhs |  120 +++++++++++++++++++---------------
 compiler/typecheck/TcUnify.lhs      |   67 +++++++++++---------
 7 files changed, 221 insertions(+), 215 deletions(-)

comment:4 Changed 2 years ago by simonpj

  • Difficulty set to Unknown
  • Resolution set to fixed
  • Status changed from new to closed
  • Test Case set to polykinds/T6036
Note: See TracTickets for help on using tickets.