Declare TF constraints in the class

This makes sure that we can report the error even when a class has no
instances.

src/Control/Monad/Infer.hs

@@ -163,6 +163,8 @@ data WhyUnsat
   | BadDefault (Var Desugared) (Type Typed)
   | forall p. (Show (Ann p), Pretty (Type p), Var p ~ Var Resolved)
       => GivenContextNotEnough (Type p)
+  | forall p. (Show (Ann p), Pretty (Type p), Var p ~ Var Resolved)
+      => GivenContextNotEnoughIn (Type p)
   | TooConcrete (Type Typed)
   | It'sQuantified
   | MagicErrors [TypeError]
@@ -725,6 +727,18 @@ instance Note TypeError Style where
               indent 2 "Could not deduce" <+> (Right <$> displayType tau)
                 <+> "from the context" <+> (Right <$> displayType ctx)
 
+  formatNote f (ArisingFrom (UnsatClassCon _ (ConImplicit why _ _ tau) (GivenContextNotEnoughIn ctx)) _) =
+    vsep [ f [annotation why]
+         , msg
+         ]
+    where
+      msg | TyCon v <- ctx, v == tyUnitName =
+              indent 2 "No instance for" <+> (Right <$> displayType tau)
+                <+> "arising from" <+> (Right <$> blameOf why)
+          | otherwise =
+              indent 2 "Could not deduce" <+> (Right <$> displayType tau)
+                <+> "from the context given in the type" <+> (Right <$> displayType ctx)
+
 
   formatNote f (ArisingFrom (UnsatClassCon _ (ConImplicit _ _ _ t) (BadDefault meth ty)) r') =
     vsep [ nest 2 $

src/Types/Infer.hs

@@ -443,11 +443,12 @@ inferProg (Open mod pre:prg) = do
 
 inferProg (c@Class{}:prg) = do
   let v = className c
-  (stmts, decls, clss, implicits) <- condemn $ inferClass c
+  (stmts, decls, clss, implicits, syms) <- condemn $ inferClass c
   first (stmts ++) <$> do
-    local (names %~ focus decls) $
-      local (classDecs . at v ?~ clss) $
-      local (classes %~ mappend implicits) $
+    local (names %~ focus decls)
+      . local (classDecs . at v ?~ clss)
+      . local (classes %~ mappend implicits)
+      . local (tySyms %~ extendTySyms syms) $
         inferProg prg
 
 inferProg (inst@Instance{}:prg) = do

src/Types/Infer/Class.hs

@@ -20,7 +20,7 @@ import Data.Spanned
 import Data.Reason
 import Data.Graph
 import Data.Maybe
-import Data.List (sortOn, partition)
+import Data.List (sortOn, partition, unzip4)
 import Data.Char
 
 import Control.Monad.State
@@ -61,7 +61,9 @@ inferClass :: forall m. MonadInfer Typed m
            -> m ( [Toplevel Typed]
                 , Telescope Typed
                 , ClassInfo
-                , ImplicitScope ClassInfo Typed )
+                , ImplicitScope ClassInfo Typed
+                , [TySymInfo]
+                )
 inferClass clss@(Class name _ ctx _ fundeps methods classAnn) = do
   let toVar :: TyConArg Typed -> Type Typed
       toVar (TyVarArg v) = TyVar v
@@ -108,17 +110,23 @@ inferClass clss@(Class name _ ctx _ fundeps methods classAnn) = do
       unwind t = pure t
 
 
-  (assocts, assocty_tele, assoct_defs) <- fmap unzip3 . for assoctys $ \meth@(AssocType method ty ann) -> do
+  (assocts, assocty_tele, assoct_defs, assoct_info) <- fmap unzip4 . for assoctys $ \meth@(AssocType method ty ann) -> do
     let replaceK by (TyPi b t) = TyPi b $ replaceK by t
         replaceK by _ = by
     checkWildcard meth ty
 
     declared <- checkAgainstKind (BecauseOf meth) ty TyType
     let ty = replaceK declared k
+    let info = TyFamInfo { _tsName = method
+                         , _tsEquations = []
+                         , _tsConstraint = Just classConstraint
+                         , _tsArgs = map argName params
+                         , _tsKind = ty }
 
     pure ( Map.singleton method (declared, ty)
          , one method ty
          , TypeDecl Private method [] (Just []) (ann, ty)
+         , info
          )
 
   ctx <- local (names %~ focus (mconcat assocty_tele <> one name k)) . for ctx $ \x -> do
@@ -250,7 +258,9 @@ inferClass clss@(Class name _ ctx _ fundeps methods classAnn) = do
     pure ( assoct_defs ++ tyDecl:map (LetStmt Public . pure) decs
          , tele <> mconcat assocty_tele
          , info
-         , scope)
+         , scope
+         , assoct_info
+         )
 inferClass _ = error "not a class"
 
 inferInstance :: forall m. MonadInfer Typed m
@@ -349,9 +359,6 @@ inferInstance inst@(Instance clss ctx instHead bindings ann) = do
         ret (TyPi _ r) = ret r
         ret r = r
 
-        argName (TyVarArg v) = v
-        argName (TyAnnArg v _) = v
-
     (declared, global_t) <- case Map.lookup var assocTySigs of
       Just x -> pure x
       Nothing -> confesses (WrongClass bind clss)
@@ -541,6 +548,11 @@ inferInstance inst@(Instance clss ctx instHead bindings ann) = do
   pure (LetStmt Public (methods ++ defaultMethods ++ [bind]):axioms, instanceName, globalInsnConTy, info, tysyms)
 inferInstance _ = error "not an instance"
 
+argName :: TyConArg p -> Var p
+argName (TyVarArg v) = v
+argName (TyAnnArg v _) = v
+
+
 addArg :: Map.Map (Var Typed) (Type Typed) -> Type Typed -> Expr Typed -> Expr Typed
 addArg skolSub ty@(TyPi (Invisible v k req) rest) ex =
   case Map.lookup v skolSub of

src/Types/Infer/Constructor.hs

@@ -30,7 +30,7 @@ inferCon vars ret con@(ArgCon ac nm t ann) = do
 
   (ty', cs) <- listen (expandType =<< resolveKind (BecauseOf con) t)
   unless (Seq.null cs) $
-    confesses (UnsatClassCon (BecauseOf con) (cs `Seq.index` 0) (GivenContextNotEnough ty'))
+    confesses (UnsatClassCon (BecauseOf con) (cs `Seq.index` 0) (GivenContextNotEnoughIn ty'))
 
   res <- closeOver' vars (BecauseOf con) $ TyArr ty' ret
   pure ((nm, res), ArgCon ac nm ty' (ann, res))
@@ -44,7 +44,7 @@ inferCon vars ret c@(GadtCon ac nm cty ann) = do
 
   (cty, cs) <- condemn $ listen (expandType =<< resolveKind (BecauseOf c) cty)
   unless (Seq.null cs) $
-    confesses (UnsatClassCon (BecauseOf c) (cs `Seq.index` 0) (GivenContextNotEnough cty))
+    confesses (UnsatClassCon (BecauseOf c) (cs `Seq.index` 0) (GivenContextNotEnoughIn cty))
 
   var <- genName
   when (countAnon cty > 1) $ dictates (gadtConManyArgs c)

tests/types/tyfun/constrained02.ml

@@ -0,0 +1,6 @@
+class foo 'a begin
+  type bar
+end
+
+type bar_box 'a =
+  | MkBox : bar 'a -> bar_box 'a

tests/types/tyfun/constrained02.out

@@ -0,0 +1,5 @@
+constrained02.ml[6:5 ..6:32]: error
+  │ 
+6 │   | MkBox : bar 'a -> bar_box 'a
+  │     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+  Could not deduce foo 'a from the context given in the type bar 'a -> bar_box 'a

tests/types/tyfun/constrained05.out

@@ -2,4 +2,4 @@ constrained05.ml[9:15 ..9:26]: error
   │ 
 9 │ type foo 'a = Foo of f2 'a
   │               ^^^^^^^^^^^^
-  Could not deduce c2 'a from the context f2 'a
+  Could not deduce c2 'a from the context given in the type f2 'a