barrucadu / coco Goto Github PK

This might be necessary, best to implement it sooner rather than later.

Preconditions should be able to use both the seed value and the free variables.

Knowing that something is neutral can actually be fairly interesting!

unifyAccum :: Bool -> (Maybe TypeEnv -> Maybe TypeEnv) -> [TypeRep] -> [TypeRep] -> Maybe TypeEnv
unifyAccum b f as bs = foldr go (Just []) (zip as bs) where
  go (tyA, tyB) (Just env) = do
    assignments <- f (unify' b tyA tyB)
    let env' = nub (env ++ assignments)
    guard $ all (\v -> length (filter ((==v) . fst) env') <= 1) tyvars
    pure env'
  go _ Nothing = Nothing

The nub / guard is too strict, it requires that type variables have equal assignments, rather than just unifying assignments. A better solution is a unifyTypeEnvs :: TypeEnv -> TypeEnv -> Maybe TypeEnv function which finds all clashes and attempts to unify them, continuing recursively if this introduces new constraints.

I've figured out a nice way to support an arbitrary number of type variables:

> :set -XDataKinds
> :set -XKindSignatures
> import Data.Proxy
> import Data.Typeable
> import GHC.TypeLits
> data TyVar (n :: Nat) = TyVar
> type A = TyVar 0
> let isTypeVar :: Typeable t => Proxy t -> Bool; isTypeVar p = fst (splitTyConApp (typeRep p)) == fst (splitTyConApp (typeRep (Proxy :: Proxy A)))
> isTypeVar (Proxy :: Proxy A)
True
> isTypeVar (Proxy :: Proxy Int)
False

The A, B, C, an D types can still be exported, but now if someone wants more they can have as many as they want.

There are two problems with the current syntax:

1. -[- is not a valid Haskell operator name, because someone could do this:

instance Num a => Num [a] where
    fromIntegral n = [fromInteger n]
    a - b = [sum a - sum b]
  ...

> 3 -[- 6 ]
 9

2. The real operator is actually read as "is refined by", not "refines". So it's backwards.

Hard to do without causing regressions. Branch wip-more-general-interference has a rough prototype.

Call out to QuickSpec or Speculate (probably Speculate, as I want conditional equations eventually)