[Haskell-cafe] Question about type inference of a GADT term

21 Sep 2012

      -----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Hello cafe,

I have the following GADT definitions capturing the simply typed
lambda calculus with de Bruijn indices for variables and explicitly
annotated types for variables:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}

- -- Typing contexts
data Ctx = CtxNil
         | CtxCons Ctx Type

- -- Types
data Type = TyInt
          | TyArrow Type Type

- -- Variable indices
data Ix (ctx :: Ctx) (ty :: Type) where
  IxZero :: Ix ctx ty
  IxSucc :: Ix ctx ty1 -> Ix (CtxCons ctx ty2) ty1

- -- Type representations
data TyRep (ty :: Type) where
  TyRepInt :: TyRep TyInt
  TyRepArrow :: TyRep ty1 -> TyRep ty2 -> TyRep (TyArrow ty1 ty2)

- -- Terms
data Term (ctx :: Ctx) (ty :: Type) where
  TmInt :: Integer -> Term ctx TyInt
  TmVar :: Ix ctx ty -> Term ctx ty
  TmAdd :: Term ctx TyInt -> Term ctx TyInt -> Term ctx TyInt
  TmApp :: Term ctx (TyArrow ty1 ty2) -> Term ctx ty1 -> Term ctx ty2
  TmAbs :: TyRep ty1 -> Term (CtxCons ctx ty1) ty2
           -> Term ctx (TyArrow ty1 ty2)

For the following definition

test1 = TmAbs TyRepInt (TmVar IxZero)

GHCi infers the type

test1 :: Term ctx (TyArrow 'TyInt ty2)

I was a bit puzzled because I expected

Term ctx (TyArrow TyInt TyInt)

Of course, this more special type is an instance of the inferred one,
so I can assign it by a type signature.

Can someone explain why the inferred type is more general?

Terms like

test2 = TmAbs TyRepInt (TmAdd (TmVar IxZero) (TmInt 5))

have the type I expected:

test2 :: Term ctx (TyArrow 'TyInt 'TyInt)

Thank you and best regards,

Florian

- -- 
Florian Lorenzen

Technische Universität Berlin
Fakultät IV - Elektrotechnik und Informatik
Übersetzerbau und Programmiersprachen

Sekr. TEL12-2, Ernst-Reuter-Platz 7, D-10587 Berlin

Tel.:   +49 (30) 314-24618
E-Mail: florian.lorenzen@tu-berlin.de
WWW:    http://www.user.tu-berlin.de/florenz/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.11 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://www.enigmail.net/

iEYEARECAAYFAlBcXs4ACgkQvjzICpVvX7b1WQCePiL+SFNj9X+U0V2fnykuatLX
pIcAn1VDNRiSR18s7UgctdPeNzFgStbi
=LBGb
-----END PGP SIGNATURE-----