"guarded instances": instance selection can add extra parameters to the class
|Reported by:||nfrisby||Owned by:||simonpj|
|Component:||Compiler (Type checker)||Version:||7.2.1|
|Type of failure:||None/Unknown||Test Case:|
|Related Tickets:||Differential Rev(s):|
Disclaimer: the same semantics can currently be achieved without this syntax. So this is mostly a Parser request, though I've made it a Type Checker request because some type errors would probably need to be aware of the language extension. More on this at the bottom.
We'll start with a demonstration. Just some ancillary declarations for now.
class Sat t where dict :: t data True; data False type family Pred (p :: * -> *) a type family Left a; type instance (Either l r) = l type family Right a; type instance (Either l r) = r data Path p a where Here :: p a -> Path p a L :: Path p l -> Path p (Either l r) R :: Path p r -> Path p (Either l r)
The objective of these declarations is to allow us to define some
p and use the
Sat class to find a path leading through a tree of
Eithers to a type that satisfies that
These next three declarations use the new syntax, as I'm imagining it.
-- NB new syntax: `guard' keyword, the pipe after the instance head, -- and a comma-separated list of types after that instance guard Sat (Path a) | Pred p a, Pred (Path p) (Left a), Pred (Path p) (Right a) -- now we match on the instance guards, using the same pipe syntax instance Sat (p a) => Sat (Path p a) | True , satl , satr where dict = Here dict instance Sat (Path p l) => Sat (Path p (Either l r)) | False, True , satr where dict = SL dict instance Sat (Path p r) => Sat (Path p (Either l r)) | False, False, True where dict = SR dict
guard declaration asserts that any instance of
Sat with a head that would overlap a la
Path a shall be disambiguated via the comma-separated list of types following the pipe. In this example, the subsequent three instances, which would traditionally overlap, are indeed disambiguated by their additional "instance head guards" (cf. HList's type-level programming style: AdvancedOverlap).
We can currently simulate this syntax by declaring a variant class of `Sat' which takes an extra parameter and thread the instance guards through that. Unfortunately, this workaround is repetitive, misses out on the better type error messages possible with specific Type Checker support, and it's just a bother.
class Sat_ a anno where dict_ :: anno -> a instance (anno ~ (Pred p a, Pred (Path p) (Left a), Pred (Path p) (Right a)), Sat_ (Found a) anno) => Sat (Path p a) where dict = dict_ (undefined :: anno) instance Sat (p a) => Sat_ (Path p a) (True, satl, satr) where dict_ _ = Here dict …
In the spirit of #4259, total type families, and AdvancedOverlap, this syntax could be enriched and thereby promoted to an actual Type Checker extension. Replacing the comma-separated list of types in the
guard declaration with a sequence of contexts would be appropriate syntax for explicitly making instance selection sensitive to those contexts. The instance head guards could then just be a type boolean (wired-in to the compiler, now) indicating whether the context was satisfied. A
True would bring that context's consequences to bear within both the instance's own context and its declarations. For example, we could do without the
Right type families.
instance guard Sat (Path a) | (Pred p a) (a ~ Either l r, Pred (Path p) l) (a ~ Either l r, Pred (Path p) r) instance Sat (p a) => Sat (Path p a) | True satl satr where dict = Here dict …