Support typechecking of type literals in backpack
authorPiyush P Kurur <ppk@cse.iitk.ac.in>
Mon, 6 Aug 2018 22:37:56 +0000 (18:37 -0400)
committerBen Gamari <ben@smart-cactus.org>
Mon, 6 Aug 2018 22:38:55 +0000 (18:38 -0400)
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

compiler/typecheck/TcRnDriver.hs
compiler/types/Type.hs
testsuite/tests/backpack/should_run/T15138.bkp [new file with mode: 0644]
testsuite/tests/backpack/should_run/T15138.stdout [new file with mode: 0644]
testsuite/tests/backpack/should_run/all.T

index 4449d67..cc9518f 100644 (file)
@@ -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)
index 3a3048d..ac1c8b9 100644 (file)
@@ -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.
diff --git a/testsuite/tests/backpack/should_run/T15138.bkp b/testsuite/tests/backpack/should_run/T15138.bkp
new file mode 100644 (file)
index 0000000..7cb9eeb
--- /dev/null
@@ -0,0 +1,36 @@
+{-# 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
diff --git a/testsuite/tests/backpack/should_run/T15138.stdout b/testsuite/tests/backpack/should_run/T15138.stdout
new file mode 100644 (file)
index 0000000..f5c8955
--- /dev/null
@@ -0,0 +1 @@
+32
index 48ed0c6..61277b8 100644 (file)
@@ -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, [''])