Skip to content

Unpromoted tuples in TH in correctly accepted by the type checker

This issue was discovered when writing tests for #11629 (closed).

Test case:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FlexibleInstances #-}
module T11629 where

import Control.Monad
import Language.Haskell.TH

class D (a :: (Bool, Bool))

instance D '(True, False)
instance D '(False, True)

do
  let getType (InstanceD _ _ ty _) = ty
      getType _                    = error "getType: only defined for InstanceD"

      failMsg a ty1 ty2 = fail $ "example " ++ a
        ++ ": ty1 /= ty2, where\n ty1 = "
        ++ show ty1 ++ "\n ty2 = " ++ show ty2

      withoutSig (ForallT tvs cxt ty) = ForallT tvs cxt (withoutSig ty)
      withoutSig (AppT ty1 ty2)       = AppT (withoutSig ty1) (withoutSig ty2)
      withoutSig (SigT ty ki)         = withoutSig ty
      withoutSig ty                   = ty

  -- test #2: type quotations and reified types should agree wrt
  -- promoted tuples.
  ty1 <- [t| D '(True, False) |]
  ty2 <- [t| D (False, True)  |]
  ClassI _ insts <- reify ''D
  let [ty1', ty2'] = map (withoutSig . getType) insts

  when (ty1 /= ty1') $ failMsg "C" ty1 ty1'
  when (ty2 /= ty2') $ failMsg "D" ty2 ty2'

  return []

According to @RyanlGlScott in https://phabricator.haskell.org/D2188#79228 the code D (True, False) in regular Haskell code would be rejected as a Kind error, whereas when its in Oxford brackets like [t| D (True, False) |], it manages to sneak through the type checker.

Edited by Ryan Scott
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information