content: {-# LANGUAGE TypeFamilies, LiberalTypeSynonyms, ImpredicativeTypes #-}
  module PolyTypeDecomp where
  
  
  {- The purpose of this test is to check if decomposition of wanted
     equalities in the /constraint solver/ (vs. the unifier) works properly.
     Unfortunately most equalities between polymorphic types are converted to
     implication constraints early on in the unifier, so we have to make things
     a bit more convoluted by introducing the myLength function. The wanted
     constraints we get for this program are:
        [forall a. Maybe a] ~ Id alpha
        [forall a. F [a]]   ~ Id alpha
     Which, /after reactions/ should create a fresh implication:
        forall a. Maybe a ~ F [a]
     that is perfectly soluble.
  -}
  
  type family F a
  type instance F [a] = Maybe a
  
  type family Id a
  type instance Id a = a
  
  f :: [forall a. F [a]]
  f = undefined
  
  
  -- This can't possibly work, even with Quick Look
  g :: [forall a. Maybe a] -> Int
  g x = myLength [x,f]
  -- [x,f] :: [[forall a. Maybe a]]
  
  myLength :: [Id a] -> Int
  myLength = undefined
  