Skip to content
Snippets Groups Projects

Figure out how to support type synonym implementions of abstract data

    • Closed Issue created by Edward Z. Yang @ezyang

    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.

    Edited
    To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information

    Child items ...

    • Activity

    Please register or sign in to reply