[commit: ghc] master: Support typechecking of type literals in backpack (7d77198)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/7d771987c2766bfedc92f5183d6fd571ab508a0e/ghc

>---------------------------------------------------------------

commit 7d771987c2766bfedc92f5183d6fd571ab508a0e
Author: Piyush P Kurur <ppk at cse.iitk.ac.in>
Date:   Mon Aug 6 18:37:56 2018 -0400

    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


>---------------------------------------------------------------

7d771987c2766bfedc92f5183d6fd571ab508a0e
 compiler/typecheck/TcRnDriver.hs                  | 12 +++++++-
 compiler/types/Type.hs                            |  6 ++++
 testsuite/tests/backpack/should_run/T15138.bkp    | 36 +++++++++++++++++++++++
 testsuite/tests/backpack/should_run/T15138.stdout |  1 +
 testsuite/tests/backpack/should_run/all.T         |  1 +
 5 files changed, 55 insertions(+), 1 deletion(-)

diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index 4449d67..cc9518f 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -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)
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 3a3048d..ac1c8b9 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -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
index 0000000..7cb9eeb
--- /dev/null
+++ b/testsuite/tests/backpack/should_run/T15138.bkp
@@ -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
index 0000000..f5c8955
--- /dev/null
+++ b/testsuite/tests/backpack/should_run/T15138.stdout
@@ -0,0 +1 @@
+32
diff --git a/testsuite/tests/backpack/should_run/all.T b/testsuite/tests/backpack/should_run/all.T
index 48ed0c6..61277b8 100644
--- a/testsuite/tests/backpack/should_run/all.T
+++ b/testsuite/tests/backpack/should_run/all.T
@@ -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, [''])