Commit 7d771987 authored by Piyush P Kurur's avatar Piyush P Kurur Committed by Ben Gamari

Support typechecking of type literals in backpack

Backpack is unable to type check signatures that expect a data which
is a type level literal. This was reported in issue #15138. These
commits are a fix for this. It also includes a minimal test case that
was mentioned in the issue.

Reviewers: bgamari, ezyang, goldfire

Reviewed By: bgamari, ezyang

Subscribers: simonpj, ezyang, rwbarton, thomie, carter

GHC Trac Issues: #15138

Differential Revision: https://phabricator.haskell.org/D4951
parent e28bb01d
......@@ -1016,7 +1016,6 @@ checkBootTyCon is_boot tc1 tc2
= ASSERT(tc1 == tc2)
checkRoles roles1 roles2 `andThenCheck`
check (eqTypeX env syn_rhs1 syn_rhs2) empty -- nothing interesting to say
-- This allows abstract 'data T a' to be implemented using 'type T = ...'
-- and abstract 'class K a' to be implement using 'type K = ...'
-- See Note [Synonyms implement abstract data]
......@@ -1031,6 +1030,17 @@ checkBootTyCon is_boot tc1 tc2
-- So for now, let it all through (it won't cause segfaults, anyway).
-- Tracked at #12704.
-- This allows abstract 'data T :: Nat' to be implemented using
-- 'type T = 42' Since the kinds already match (we have checked this
-- upfront) all we need to check is that the implementation 'type T
-- = ...' defined an actual literal. See #15138 for the case this
-- handles.
| not is_boot
, isAbstractTyCon tc1
, Just (_,ty2) <- synTyConDefn_maybe tc2
, isJust (isLitTy ty2)
= Nothing
| Just fam_flav1 <- famTyConFlav_maybe tc1
, Just fam_flav2 <- famTyConFlav_maybe tc2
= ASSERT(tc1 == tc2)
......
......@@ -48,6 +48,7 @@ module Type (
mkNumLitTy, isNumLitTy,
mkStrLitTy, isStrLitTy,
isLitTy,
getRuntimeRep_maybe, getRuntimeRepFromKind_maybe,
......@@ -856,6 +857,11 @@ isStrLitTy ty | Just ty1 <- coreView ty = isStrLitTy ty1
isStrLitTy (LitTy (StrTyLit s)) = Just s
isStrLitTy _ = Nothing
-- | Is this a type literal (symbol or numeric).
isLitTy :: Type -> Maybe TyLit
isLitTy ty | Just ty1 <- coreView ty = isLitTy ty1
isLitTy (LitTy l) = Just l
isLitTy _ = Nothing
-- | Is this type a custom user error?
-- If so, give us the kind and the error message.
......
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
unit indef where
signature Abstract where
import GHC.TypeLits
data NatType :: Nat
module Util where
import Abstract
import Data.Proxy
import GHC.TypeLits
natTypeToInteger :: KnownNat NatType => Proxy NatType -> Integer
natTypeToInteger = natVal
unit concrete where
module Concrete where
type NatType = 32
unit main where
dependency indef[Abstract=concrete:Concrete] (Util as MyUtil)
module Main where
import Data.Proxy
import MyUtil
main :: IO ()
main = do print $ natTypeToInteger Proxy
......@@ -8,3 +8,4 @@ test('bkprun07', normal, backpack_run, [''])
test('bkprun08', normal, backpack_run, [''])
test('bkprun09', normal, backpack_run, ['-O'])
test('T13955', normal, backpack_run, [''])
test('T15138', normal, backpack_run, [''])
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment