Trouble refactoring current types(possibly GADT/Type Families related)

I've got types like this:

-- There are codes
newtype ICode = ICode { fromICode :: String }
newtype RCode = RCode { fromRCode :: String }
data DCode = DCode1 | DCode2 | DCode3

-- There are locations described by type and code.
-- Current implementation looks like this:
data Location = LocType1 ICode
              | LocType2 ICode
              | LocType3 RCode
              | LocType4 DCode

I'd like to refactor these types to address some problems, which are present in current implementation.

It's real easy to demonstrate the properties I'm after with QuickCheck Arbitrary and Aeson's FromJSON instances and one other function. First 3 properties are needed to generate correct test data and 4th to implement business logic.

I'd like to be able to:

make Arbitrary instances of all code types such as

    instance Arbitrary ICode where
      arbitrary = ...
    -- same with RCode and DCode

make Arbitrary instances of types like Location1 ICode(It clearly differs from current implementation and it's what I'm trying to fix), which describe exact combination of location type and code type. Location1 ICode can contain only a subset of ICode possible values, so I have to make sure of that.
make FromJSON instances of all possible types, something in the lines of:
```
instance FromJSON (Location a) where
  parseJSON = ...
```
It's needed to deserialize some json objects depending on their values.
Some functions have to work only on one location type. It's pretty inconvenient in current implementation, because I have to use either incomplete functions or not really correct return types such as Maybe. I'd like to be able to do something like:
```
location1IncludedInArbitraryLocation :: LocType1 -> Location a -> Bool
location1IncludedInArbitraryLocation l = ...
```

I believe solution lies somewhere in the GADTs/Data Families territory, but I'm not really fluent with this kind of type-fu. If several ways to resolve this issue are possible, which one would be easier to typecheck/work with later?

Solution

3 and 4 seem incompatible. This sounds like a "fallback" mechanism: use this instance if no more specific instance is available. You can get this with OverlappingInstances, but I always seem to run into trouble with it. Worth a shot, I guess.

As for the rest of your problem, it seems like you want Location to be a GADT.

data LocType = Type1 | Type2 | Type3 | Type4

data Location :: LocType -> * where
    LocType1 :: ICode -> Location Type1
    LocType2 :: ICode -> Location Type2
    LocType3 :: RCode -> Location Type3
    LocType4 :: DCode -> Location Type4

Then you can easily do:

location1IncludedInArbitraryLocation :: Location Type1 -> Location t -> Bool
location1IncludedInArbitraryLocation (LocType1 icode) l = ...

No other cases need be defined here because no other constructor will be well-typed.

I hope this gives you enough to start playing with.

(Needs DataKinds, KindSignatures, GADTs)