#10725: Figure out how to support type synonym implementions of abstract data -------------------------------------+------------------------------------- Reporter: ezyang | Owner: ezyang Type: task | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Description changed by ezyang: Old description:

A classic example we have used when describing Backpack is that you might want to abstract over is different types of strings: String, ByteString, Text, etc.

Unfortunately, with every implementation of Backpack we have had so far, you can't actually do this! For example, say you use a type synonym to get an existing data type to the "right name"; you get this error:

{{{ A.hs-boot:2:6: Type constructor `T' has conflicting definitions in the module and its hs-boot file Main module: type T = String Boot file: abstract(False) T No C type associated RecFlag NonRecursive FamilyInstance: none }}}

How can we make this work? Could it be as simple as just relaxing the restriction here? This seems to work OK with shaping, so long as we refer to the type synonym (and not the original type in question!) If some type checker experts could weight in that would be quite useful.

----

Probably the biggest danger is interaction with machinery that works with type families. For example, this is accepted:

{{{ -- A.hs-boot module A where data T

-- B.hs {-# LANGUAGE TypeFamilies #-} module B where import {-# SOURCE #-} qualified A

data T = T

type family F a :: * type instance F A.T = Bool type instance F T = Int }}}

This doesn't lead to unsoundness today, because A.T must always be defined in A.hs (and thus have a unique nominal identity). But it's dangerous for this to be accepted today with signatures, since T could refer to B.T. (The moral of the story is that after shaping, you have to recheck all pairs of families; you can't assume that because they were typechecked earlier that they're OK.)

New description: A classic example we have used when describing Backpack is that you might want to abstract over is different types of strings: String, ByteString, Text, etc. Unfortunately, with every implementation of Backpack we have had so far, you can't actually do this! For example, say you use a type synonym to get an existing data type to the "right name"; you get this error: {{{ A.hs-boot:2:6: Type constructor `T' has conflicting definitions in the module and its hs-boot file Main module: type T = String Boot file: abstract(False) T No C type associated RecFlag NonRecursive FamilyInstance: none }}} How can we make this work? Could it be as simple as just relaxing the restriction here? This seems to work OK with shaping, so long as we refer to the type synonym (and not the original type in question!) If some type checker experts could weight in that would be quite useful. ---- Probably the biggest danger is interaction with machinery that works with type families. For example, this is accepted: {{{ -- A.hs-boot module A where data T -- B.hs {-# LANGUAGE TypeFamilies #-} module B where import {-# SOURCE #-} qualified A data T = T type family F a :: * type instance F A.T = Bool type instance F T = Int }}} This doesn't lead to unsoundness today, because A.T must always be defined in A.hs (and thus have a unique nominal identity). But with synonyms (or even hs-boot files that don't have the "defined in the implementing module" requirement) it's dangerous; we need to notice that the type instance is inconsistent when we finally see the implementation. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10725#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10725: Figure out how to support type synonym implementions of abstract data -------------------------------------+------------------------------------- Reporter: ezyang | Owner: ezyang Type: task | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: fixed | Keywords: backpack Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by ezyang): * status: new => closed * resolution: => fixed Comment: It was really easy, and I've implemented it on my branch. Just a few minor complications: 1. When we recompile an hsig file with the actual backing implementation, we need to notice when we define an abstract type "data A" which is implemented with a type synonym, and "swap in" the correct type synonym immediately. If we don't, when we subsequently refer to A we'll get a TyCon that is not decorated as a type synonym (despite being the same original name as a type synonym), and then type equality chokes. 2. There was a bug when serializing out hsig interface files where I was incorrectly grabbing fingerprints locally rather than from the backing implementation. That's fixed now. https://github.com/ezyang/ghc/commit/4d59c74b2381eb8e2b9c1d31111a921ed95ebd2... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10725#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler