#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